The nonarithmeticity of the predicate logicof primitive recursive realizability
- Authors: Plisko V.E.1
-
Affiliations:
- Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
- Issue: Vol 87, No 2 (2023)
- Pages: 196-228
- Section: Articles
- URL: https://journals.rcsi.science/1607-0046/article/view/133916
- DOI: https://doi.org/10.4213/im9288
- ID: 133916
Cite item
Open Access
Access granted
Subscription Access
Abstract
The notion of primitive recursive realizability was introducedby S. Salehi as a kind of semantics for the language of basic arithmeticusing primitive recursive functions. It is of interest to studythe corresponding predicate logic. D. A. Viter proved that the predicatelogic of primitive recursive realizability by Salehi is not arithmetical.The technically complex proof combines the methods used by the authorof this article in the study of predicate logics of constructive arithmetictheories and the results of M. Ardeshir on the translation ofthe intuitionistic predicate logic into the basic predicate logic.The purpose of this article is to present another proof of Viter's resultby directly transferring the methods used earlier in provingthe nonarithmeticity of the predicate logic of recursive realizability.
About the authors
Valerii Egorovich Plisko
Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
Email: veplisko@yandex.ru
Candidate of physico-mathematical sciences, Associate professor
References
- S. C. Kleene, “On the interpretation of intuitionistic number theory”, J. Symbolic Logic, 10:4 (1945), 109–124
- С. К. Клини, Введение в метаматематику, ИЛ, М., 1957, 526 с.
- 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
- S. Salehi, “Provably total functions of basic arithmetic”, MLQ Math. Log. Q., 49:3 (2003), 316–322
- A. Visser, “A propositional logic with explicit fixed points”, Studia Logica, 40:2 (1981), 155–175
- W. Ruitenburg, “Basic predicate calculus”, Notre Dame J. Formal Logic, 39:1 (1998), 18–46
- В. Е. Плиско, “Неарифметичность класса реализуемых предикатных формул”, Изв. АН СССР. Сер. матем., 41:3 (1977), 483–502
- Д. А. Витер, Примитивно рекурсивная реализуемость и конструктивная теория моделей, Дисс. … канд. физ.-матем. наук, МГУ, М., 2002, 150 с.
- В. Е. Плиско, “Конструктивная формализация теоремы Тенненбаума и ее применения”, Матем. заметки, 48:3 (1990), 108–118
- M. Ardeshir, “A translation of intuitionistic predicate logic into basic predicate logic”, Studia Logica, 62 (1999), 341–352
- Д. А. Витер, Примитивно рекурсивная реализуемость и логика предикатов, Рукопись деп. в ВИНИТИ, № 1830, ВИНИТИ, М., 2001
- Z. Damnjanovic, “Strictly primitive recursive realizability. I”, J. Symbolic Logic, 59:4 (1994), 1210–1227
- В. Е. Плиско, “О соотношении двух понятий примитивно рекурсивной реализуемости”, Вестн. Моск. ун-та. Сер. 1. Матем., мех., 2006, № 1, 6–11
- Б. Х. Пак, Субрекурсивная реализуемость и логика предикатов, Дисс. … канд. физ.-матем. наук, МГУ, М., 2003, 83 с.
- Б. Х. Пак, Строго примитивно рекурсивная реализуемость и логика предикатов, Рукопись деп. в ВИНИТИ, № 218-В2003, ВИНИТИ, М., 2003
- 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
- V. Plisko, “The nonarithmeticity of the predicate logic of strictly primitive recursive realizability”, Rev. Symb. Log., 15:3 (2022), 693–721
- S. Kleene, “Extension of an effectively generated class of functions by enumeration”, Colloq. Math., 6 (1958), 67–78
- В. Е. Плиско, “Об арифметической сложности предикатных логик полных конструктивных арифметических теорий”, Фундамент. и прикл. матем., 5:1 (1999), 221–255
Supplementary files
