Geodesic
The nonarithmeticity of the predicate logic
Izvestiya. Mathematics , Tome 87 (2023) no. 2, pp. 389-419.

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

The notion of primitive recursive realizability was introduced by S. Salehi as a kind of semantics for the language of basic arithmetic using primitive recursive functions. It is of interest to study the corresponding predicate logic. D. A. Viter proved that the predicate logic of primitive recursive realizability by Salehi is not arithmetical. The technically complex proof combines the methods used by the author of this article in the study of predicate logics of constructive arithmetic theories and the results of M. Ardeshir on the translation of the intuitionistic predicate logic into the basic predicate logic. The purpose of this article is to present another proof of Viter's result by directly transferring the methods used earlier in proving the nonarithmeticity of the predicate logic of recursive realizability.
Keywords: predicate logic, primitive recursive realizability, basic arithmetic, basic predicate logic, nonarithmeticity. 
@article{IM2_2023_87_2_a6,
     author = {V. E. Plisko},
     title = {The nonarithmeticity of the predicate logic},
     journal = {Izvestiya. Mathematics },
     pages = {389--419},
     publisher = {mathdoc},
     volume = {87},
     number = {2},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IM2_2023_87_2_a6/}
}
TY  - JOUR
AU  - V. E. Plisko
TI  - The nonarithmeticity of the predicate logic
JO  - Izvestiya. Mathematics 
PY  - 2023
SP  - 389
EP  - 419
VL  - 87
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IM2_2023_87_2_a6/
LA  - en
ID  - IM2_2023_87_2_a6
ER  - 
%0 Journal Article
%A V. E. Plisko
%T The nonarithmeticity of the predicate logic
%J Izvestiya. Mathematics 
%D 2023
%P 389-419
%V 87
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IM2_2023_87_2_a6/
%G en
%F IM2_2023_87_2_a6
V. E. Plisko. The nonarithmeticity of the predicate logic. Izvestiya. Mathematics , Tome 87 (2023) no. 2, pp. 389-419. http://geodesic.mathdoc.fr/item/IM2_2023_87_2_a6/

[1] S. C. Kleene, “On the interpretation of intuitionistic number theory”, J. Symbolic Logic, 10:4 (1945), 109–124 | DOI | MR | Zbl

[2] S. C. Kleene, Introduction to metamathematics, D. Van Nostrand Co., Inc., New York, NY, 1952 ; Russian transl. Inostr. Lit., Moscow, 1957 | MR | Zbl | MR

[3] S. Salehi, “Primitive recursive realizability and basic arithmetic”, in “2000 European summer meeting of the association for symbolic logic. Logic colloquium 2000”, Bull. Symbolic Logic, 7 (2001), 147–148 | DOI | Zbl

[4] S. Salehi, “Provably total functions of basic arithmetic”, MLQ Math. Log. Q., 49:3 (2003), 316–322 | DOI | MR | Zbl

[5] A. Visser, “A propositional logic with explicit fixed points”, Studia Logica, 40:2 (1981), 155–175 | DOI | MR | Zbl

[6] W. Ruitenburg, “Basic predicate calculus”, Notre Dame J. Formal Logic, 39:1 (1998), 18–46 | DOI | MR | Zbl

[7] V. E. Plisko, “The nonarithmeticity of the class of realizable predicate formulas”, Izv. Akad. Nauk SSSR Ser. Mat., 41:3 (1977), 483–502 ; English transl. Izv. Math., 11:3 (1977), 453–471 | MR | Zbl | DOI

[8] D. A. Viter, Primitive recursive realizability and constructive model theory, Diss. Cand. Phys.-Math. Sci., Moscow Univ., Moscow, 2002

[9] V. E. Plisko, “Constructive formalization of the Tennenbaum theorem and its applications”, Mat. Zametki, 48:3 (1990), 108–118 ; English transl. Math. Notes, 48:3 (1990), 950–957 | MR | Zbl | DOI

[10] M. Ardeshir, “A translation of intuitionistic predicate logic into basic predicate logic”, Studia Logica, 62 (1999), 341–352 | DOI | MR | Zbl

[11] D. A. Viter, Primitive recursive realizability and predicate logic, Deposited in VINITI, no. 1830, VINITI, Moscow, 2001

[12] Z. Damnjanovic, “Strictly primitive recursive realizability. I”, J. Symbolic Logic, 59:4 (1994), 1210–1227 | DOI | MR | Zbl

[13] V. E. Plisko, “A relationship between two notions of primitive recursive realizability”, Vestnik Moskov. Univ. Ser. 1. Mat. Mekh., 2006, no. 1, 6–11 ; English transl. Moscow Univ. Math. Bull., 61:1 (2006), 5–11 | MR | Zbl

[14] B. H. Park, Subrecursive realizability and predicate logic, Diss. Cand. Phys.-Math. Sci., Moscow Univ., Moscow, 2003

[15] B. H. Park, Strictly primitive recursive realizability and predicate logic, Deposited in VINITI, no. 218-B2003, VINITI, Moscow, 2003

[16] V. Plisko, “On primitive recursive realizabilities”, Computer science – theory and applications, Proceedings of the 1st international symposium on computer science (CSR 2006) (St. Petersburg 2006), Lecture Notes in Comput. Sci., 3967, Springer, Berlin, 2006, 304–312 | DOI | MR | Zbl

[17] V. Plisko, “The nonarithmeticity of the predicate logic of strictly primitive recursive realizability”, Rev. Symb. Log., 15:3 (2022), 693–721 | DOI | MR | Zbl

[18] S. Kleene, “Extension of an effectively generated class of functions by enumeration”, Colloq. Math., 6 (1958), 67–78 | DOI | MR | Zbl

[19] V. E. Plisko, “On arithmetic complexity of the predicate logics of complete constructive arithmetic theories”, Fundam. Prikl. Mat., 5:1 (1999), 221–255 | MR | Zbl