Arithmetic complexity of the predicate logics of certain complete arithmetic theories (Q5957916)

Each arithmetic theory obtained by adding the Markov principle \(\forall x(A\vee\neg A)\wedge\neg\neg\exists xA\to\exists xA\) and the Church thesis \(\forall x\exists yA(x,y)\to\exists z\forall xA(x,\{z\}(x))\), where \(\{z\}\) denotes the partial recursive function with index \(z\), to the Heyting arithmetic, is a constructive arithmetic theory. The central result presented in this paper is that the predicate logic of each complete constructive arithmetic theory \(T\), having the existential property, is \(\Pi^T_1\)-complete. In order to prove this, the author uses the technique of uniform partial truth definition for intuitionistic theories and applies the main theorem to the characterization of the predicate logic corresponding to a certain variant of the notion of realizable predicate formula. More accurrately, it is shown that the set of irrefutable formulas is recursively isomorphic to the complement of the set \(\emptyset^{(\omega+1)}\). The notion of \(\Sigma_n\)-realizability is defined on the basis of the notion of a \(\Sigma_n\)-function and it is proved that the predicate logic of \(\Sigma_n\)-realizability is \(\Pi_{\omega+1}\)-hard.