Arithmetic complexity of the predicate logics of certain complete arithmetic theories

DOI10.1016/S0168-0072(01)00061-6MaRDI QIDQ5957916zbMATH OpenFDO

Authors Valery Plisko

Publication date 5 September 2002

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0168-0072(01)00061-6

zbMATH Keywords

arithmetic hierarchy constructive arithmetic theory constructive logic partial truth definition

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Intuitionistic mathematics (03F55)

Review text

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.

Recommendations

Cites work

Cited in

(14)

This page was built for publication: Arithmetic complexity of the predicate logics of certain complete arithmetic theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5957916)