Неарифметичность предикатной логики примитивно рекурсивной реализуемости
- Авторы: Плиско В.Е.1
-
Учреждения:
- Московский государственный университет имени М. В. Ломоносова, механико-математический факультет
- Выпуск: Том 87, № 2 (2023)
- Страницы: 196-228
- Раздел: Статьи
- URL: https://journal-vniispk.ru/1607-0046/article/view/133916
- DOI: https://doi.org/10.4213/im9288
- ID: 133916
Цитировать
Открытый доступ
Доступ предоставлен
Только для подписчиков
Аннотация
Понятие примитивно рекурсивной реализуемости было введено С. Салехи как своего рода семантика для языка базисной арифметики с использованием примитивно рекурсивных функций. Представляет интерес изучение соответствующей логики предикатов. Д. А. Витер доказал, что предикатная логика примитивно рекурсивной реализуемости Салехи не является арифметической. Технически сложное доказательство сочетает в себе методы, использованные автором настоящей статьи при изучении предикатных логик конструктивных арифметических теорий, и результаты М. Ардешира по переводу интуиционистской логики предикатов в базисную логику предикатов. Цель этой статьи — представить другое доказательство результата Витера путем прямого переноса методов, использованных ранее в доказательстве неарифметичности предикатной логики рекурсивной реализуемости.Библиография: 19 наименований.
Об авторах
Валерий Егорович Плиско
Московский государственный университет имени М. В. Ломоносова, механико-математический факультет
Email: veplisko@yandex.ru
кандидат физико-математических наук, доцент
Список литературы
- 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
Дополнительные файлы
