A survey of predicate realizability logic

Valerii E. Plisko

Trudy Matematicheskogo Instituta imeni V.A. Steklova, Algorithmic aspects of algebra and logic, Tome 274 (2011), pp. 222-251.

Résumé

The paper contains a survey of the results and methods of studying interpretations of predicate formulas based on constructive semantics of the first-order language of arithmetic and its extensions.

Bibliographie

[1] Vardanyan V.A., O predikatnoi logike dokazuemosti, Preprint, Nauch. sovet po kompleksnoi probleme “Kibernetika”, M., 1985 | MR

[2] Gëdel K., “Ob odnom esche ne ispolzovannom rasshirenii finitnoi tochki zreniya”, Matematicheskaya teoriya logicheskogo vyvoda, Nauka, M., 1967, 299–310 | MR

[3] Gilbert D., Bernais P., Osnovaniya matematiki: Teoriya dokazatelstv, Nauka, M., 1982 | MR

[4] Dragalin A.G., Matematicheskii intuitsionizm. Vvedenie v teoriyu dokazatelstv, Nauka, M., 1979 | MR | Zbl

[5] Ershov Yu.L., Problemy razreshimosti i konstruktivnye modeli, Nauka, M., 1980 | MR

[6] Zaslavskii I.D., “O nekotorykh razlichiyakh mezhdu bazisnymi i podchinennymi peremennymi v logiko-matematicheskikh yazykakh”, Matematicheskie voprosy kibernetiki i vychislitelnoi tekhniki, AN ArmSSR, Erevan, 1963, 71–80

[7] Kipnis M.M., “Konstruktivnaya klassifikatsiya arifmeticheskikh predikatov i semanticheskie bazisy arifmetiki”, Zap. nauch. sem. LOMI, 8 (1968), 53–65 | MR | Zbl

[8] Kipnis M.M., “O realizatsiyakh predikatnykh formul”, Zap. nauch. sem. LOMI, 20 (1971), 40–48 | MR | Zbl

[9] Klini S.K., Vvedenie v metamatematiku, Izd-vo inostr. lit., M., 1957 | MR

[10] Kolmogorov A.N., “O printsipe tertium non datur”, Mat. sb., 32:4 (1925), 646–667 | MR | Zbl

[11] Kolmogorov A.N., Izbrannye trudy. T. 1: Matematika i mekhanika, Nauka, M., 2005 | MR

[12] Koen P.Dzh., Teoriya mnozhestv i kontinuum-gipoteza, Mir, M., 1969 | MR

[13] Markov A.A., “O nepreryvnosti konstruktivnykh funktsii”, UMN, 9:3 (1954), 226–230 | MR | Zbl

[14] Markov A.A., “Ob odnom printsipe konstruktivnoi matematicheskoi logiki”, Tr. 3-go Vsesoyuz. mat. s'ezda, T. 2, Izd-vo AN SSSR, M., 1956, 146–147

[15] Mendelson E., Vvedenie v matematicheskuyu logiku, Nauka, M., 1971 | MR

[16] Orevkov V.P., “Svyaz konstruktivnoi obscheznachimosti s vyvodimostyu v klassicheskom ischislenii predikatov”, Vsesoyuznyi simpozium po matematicheskoi logike, Tez. dokl., Alma-Ata, 1969, 35

[17] Plisko V.E., “O realizuemykh predikatnykh formulakh”, DAN SSSR, 212:3 (1973), 553–556 | MR | Zbl

[18] Plisko V.E., “Rekursivnaya realizuemost i konstruktivnaya logika predikatov”, DAN SSSR, 214:3 (1974), 520–523 | MR | Zbl

[19] Plisko V.E., “Nearifmetichnost klassa realizuemykh predikatnykh formul”, Izv. AN SSSR. Ser. mat., 41:3 (1977), 483–502 | MR | Zbl

[20] Plisko V.E., “Nekotorye varianty ponyatiya realizuemosti dlya predikatnykh formul”, Izv. AN SSSR. Ser. mat., 42:3 (1978), 636–653 | MR

[21] Plisko V.E., “Absolyutnaya realizuemost predikatnykh formul”, Izv. AN SSSR. Ser. mat., 47:2 (1983), 315–334 | MR

[22] Plisko V.E., “O yazykakh s konstruktivnymi logicheskimi svyazkami”, DAN SSSR., 296:1 (1987), 35–38 | MR

[23] Plisko V.E., “Konstruktivnaya formalizatsiya teoremy Tennenbauma i ee primeneniya”, Mat. zametki, 48:3 (1990), 108–118 | MR | Zbl

[24] Plisko V.E., “O sootnoshenii nekotorykh ponyatii konstruktivnoi teorii modelei”, Vestn. Mosk. un-ta. Matematika. Mekhanika, 1991, no. 4, 38–41 | MR | Zbl

[25] Plisko V.E., Formalizatsiya teoremy Tennenbauma i ee primeneniya, Dep. v VINITI, No1853-B92, M., 1992

[26] Plisko V.E., “Ob arifmeticheskoi slozhnosti nekotorykh predikatnykh logik”, Mat. zametki, 52:1 (1992), 94–104 | MR | Zbl

[27] Plisko V.E., “Modifitsirovannaya realizuemost i logika predikatov”, Mat. zametki, 61:2 (1997), 259–269 | DOI | MR | Zbl

[28] Plisko V.E., “Ob arifmeticheskoi slozhnosti predikatnykh logik polnykh konstruktivnykh arifmeticheskikh teorii”, Fund. i prikl. matematika, 5:1 (1999), 221–255 | MR | Zbl

[29] Plisko V.E., “Nachala konstruktivnoi teorii modelei”, Fund. i prikl. matematika, 8:3 (2002), 783–828 | MR | Zbl

[30] Rodzhers Kh., Teoriya rekursivnykh funktsii i effektivnaya vychislimost, Mir, M., 1972 | MR

[31] Yavorskii R.E., “Razreshimye logiki pervogo poryadka”, Fund. i prikl. matematika, 4:2 (1998), 733–749 | MR

[32] Kleene S.C., “On the interpretation of intuitionistic number theory”, J. Symb. Log., 10 (1945), 109–124 | DOI | MR | Zbl

[33] Kleene S.C., “Logical calculus and realizability”, Acta philos. Fenn., 18 (1965), 71–80 | MR | Zbl

[34] Kreisel G., “Interpretation of analysis by means of constructive functionals of finite types”, Constructivity in mathematics, eds. A. Heyting, North-Holland, Amsterdam, 1959, 101–128 | MR

[35] Nelson D., “Recursive functions and intuitionistic number theory”, Trans. Amer. Math. Soc., 61 (1947), 307–368 | DOI | MR | Zbl

[36] Plisko V., “Two semantics and logics based on the Gödel interpretation”, Computational logic and proof theory, Proc. 5th Kurt Gödel Colloq., KGC'97, Vienna, 1997, Lect. Notes Comput. Sci., 1289, eds. G. Gottlob, A. Leitsch, D. Mundici, Springer, Berlin, 1997, 233–240 | DOI | MR | Zbl

[37] Plisko V., “Transfinite sequences of constructive predicate logics”, Computer science—theory and applications, Proc. 5th Intern. Comput. Sci. Symp. Russia, CSR 2010, Kazan (Russia), June 16–20, 2010, Lect. Notes Comput. Sci., 6072, eds. F. Ablayev, E.W. Mayr, Springer, Berlin, 2010, 315–326 | DOI | MR | Zbl

[38] Plisko V.E., “A survey of propositional realizability logic”, Bull. Symb. Log., 15 (2009), 1–42 | DOI | MR | Zbl

[39] Rose G.F., “Propositional calculus and realizability”, Trans. Amer. Math. Soc., 75 (1953), 1–19 | DOI | MR | Zbl

[40] Tennenbaum S., “Non-Archimedian models for arithmetic”, Not. Amer. Math. Soc., 6:3 (1959), 270

[41] Visser A., “Propositional logics of closed and open substitutions over Heyting's arithmetic”, Notre Dame J. Formal Logic., 47 (2006), 299–309 | DOI | MR | Zbl