 Both rules are also admissible for \(\mathbf{HA}.\) The corresponding implications (MP and IP respectively), which are not provable intuitionistically, are verified by Gödel’s “Dialectica” interpretation of \(\mathbf{HA}\) (cf. Section 6.3 below). So is the implication (CT) corresponding to one of the most interesting admissible rules of Heyting arithmetic, let us call it the Church-Kleene Rule: 