Geodesic
On arithmetic complexity of the predicate logics of complete constructive arithmetic theories
Fundamentalʹnaâ i prikladnaâ matematika, Tome 5 (1999) no. 1, pp. 221-255 
V. E. Plisko. On arithmetic complexity of the predicate logics of complete constructive arithmetic theories. Fundamentalʹnaâ i prikladnaâ matematika, Tome 5 (1999) no. 1, pp. 221-255. http://geodesic.mathdoc.fr/item/FPM_1999_5_1_a12/
@article{FPM_1999_5_1_a12,
     author = {V. E. Plisko},
     title = {On~arithmetic complexity of the~predicate logics of complete constructive arithmetic theories},
     journal = {Fundamentalʹna\^a i prikladna\^a matematika},
     pages = {221--255},
     year = {1999},
     volume = {5},
     number = {1},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/FPM_1999_5_1_a12/}
}
TY  - JOUR
AU  - V. E. Plisko
TI  - On arithmetic complexity of the predicate logics of complete constructive arithmetic theories
JO  - Fundamentalʹnaâ i prikladnaâ matematika
PY  - 1999
SP  - 221
EP  - 255
VL  - 5
IS  - 1
UR  - http://geodesic.mathdoc.fr/item/FPM_1999_5_1_a12/
LA  - ru
ID  - FPM_1999_5_1_a12
ER  - 
%0 Journal Article
%A V. E. Plisko
%T On arithmetic complexity of the predicate logics of complete constructive arithmetic theories
%J Fundamentalʹnaâ i prikladnaâ matematika
%D 1999
%P 221-255
%V 5
%N 1
%U http://geodesic.mathdoc.fr/item/FPM_1999_5_1_a12/
%G ru
%F FPM_1999_5_1_a12

Voir la notice de l'article provenant de la source Math-Net.Ru

It is proved in this paper that the predicate logic of each complete constructive arithmetic theory $T$ having the existence property is $\Pi_1^T$-complete. In this connection the techniques of uniform partial truth definition for intuitionistic arithmetic theories is used. The main theorem is applied to the characterization of the predicate logic corresponding to certain variant of the notion of realizable predicate formula. Namely it is shown that the set of undisprovable predicate formulas is recursively isomorphic to the complement of the set $\emptyset^{(\omega +1)}$.