 Not every admissible predicate rule of \(\mathbf{IQC}\) is admissible for all formal systems based on \(\mathbf{IQC};\) for example, \(\mathbf{HA}\) evidently violates the rule just stated. Visser proved in [1999] that the property of being an admissible predicate rule of \(\mathbf{HA}\) is \(\Pi_2\) complete, and in [2002] that \(\mathbf{HA}\) \(+\) MP has the same predicate admissible rules as \(\mathbf{HA}.\) Plisko [1992] proved that the predicate logic of \(\mathbf{HA}\) \(+\) MP (the set of sentences in the language of \(\mathbf{IQC}\) all of whose uniform substitution instances in the language of arithmetic are provable in \(\mathbf{HA}\) \(+\) MP) is \(\Pi_2\) complete; Visser [2006] extended this result to some constructively interesting consistent extensions of \(\mathbf{HA}\) which are not contained in \(\mathbf{PA}.\)