Некоторые специальные случаи интерполяционной теоремы для интуиционистского исчисления предикатов
https://doi.org/10.22405/2226-8383-2025-26-4-212-223
Аннотация
Заметка посвящена доказательству некоторых вариантов интерполяционной теоремы для интуиционистского исчисления предикатов без функциональных символов и равенства с интерполянтом специального вида. Наиболее интересен случай универсального хорновского интерполянта: аксиомы многих алгебраических систем задаются универсальными хорновскими формулами. Результаты, полученные в данной работе, могут быть полезны как с точки зрения теории доказательств, так и в приложениях, например, при решении задач искусственного интеллекта и разработке языков логического программирования. Заметка написана в духе теории доказательств, основным инструментом для решения задачи
служат секвенциальные исчисления и такие техники преобразования выводов, как обращение применений правил вывода, перестановка применений правил по С. К. Клини и прополка по В. П. Оревкову.
Заметка состоит из введения, разбитой на 3 параграфа основной части и заключения. Введение содержит краткий исторический обзор и обсуждение актуальности работы. В
первом параграфе основной части вводятся необходимые определения и формулируется главный результат. Второй параграф посвящён описанию построенного В. П. Оревковым секвенциального варианта интуиционистского исчисления предикатов IGL. Третий отведён доказательству основной теоремы. Заключение содержит обсуждение полученных результатов и краткий обзор перспектив дальнейшей работы.
Об авторе
Дмитрий Алексеевич Цибульский
Санкт-Петербургское отделение Математического института имени В. А. Стеклова РАН
Россия
Россия
аспирант
Список литературы
1. Craig W. Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem // Journal of Symbolic Logic. — 1957. — Vol. 22. — P. 250–268.
2. Lyndon R. C. An Interpolation Theorem in the Predicate Calculus // Pacific Journal of Mathematics. — 1959. — Vol. 9. — P. 129–142.
3. Sch¨utte K. Der Interpolationssatz der intuitionistischen Pr¨adikatenlogik // Mathematische Annalen. — 1962. — Vol. 148. — P. 192–200.
4. Максимова Л. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых алгебр // Алгебра и логика. — 1977. — Т. 16, № 6. — С. 643–681.
5. Maksimova L. On Variable Separation in Modal and Superintuitionistic Logics // Studia Logica. — 1995. — Vol. 55. — P. 99–112.
6. Beth E. W. On Padoa’s Method in the Theory of Definition // Indagationes Mathematicae. — 1953. — Vol. 56. — P. 330–339.
7. Robinson A. A Result of Consistency and Its Application to the Theory of Definition // Koninklijke Nederlandse Akademie van Wetenschappen. Proceedings. Series A. — 1956. — Vol. 59. — P. 47–58.
8. Kleene S. C. Mathematical Logic. — New York: John Wiley & Sons, 1967. — 394–441 p.
9. Troelstra A. S., Schwichtenberg H. Basic Proof Theory. — Cambridge: Cambridge University Press, 2000. — 116–126 p.
10. Цибульский Д. А. Специальные случаи интерполяционной теоремы для классического исчисления предикатов // Чебышевский сборник. — 2024. — Т. 25, № 2. — С. 222–234.
11. Оревков В. П. Верхние оценки удлинения выводов при устранении сечений // Записки научных семинаров ЛОМИ. — 1984. — Т. 137. — С. 87–98.
12. Оревков В. П. О гливенковских классах секвенций // Труды Математического института имени В. А. Стеклова. — 1976. — Т. 98. — С. 131–154.
13. Ершов Ю. Л., Палютин Е. А. Математическая логика. — М.: Наука, 1987. — 209–214 с.
14. Gentzen G. Untersuchungen ¨uber das logische Schließen. I, II // Mathematische Zeitschrift. — 1934. — Vol. 39. — P. 176–210, 405–443.
15. Kleene S. C. Permutability of Inferences in Gentzen’s Calculi LK and LJ // Memoirs of the American Mathematical Society. — 1952. — Vol. 10. — P. 1–26.
16. Maehara S. On the Interpolation Theorem of Craig // Sugaku. — 1960. — Vol. 12. — P. 235–237.
17. Maehara S., Takeuti G. A Formal System of First-order Predicate Calculus With Infinitely Long Expressions // Journal of the Mathematical Society of Japan. — 1961. — Vol. 13. — P. 357–370.
Рецензия
Для цитирования:
Цибульский Д.А. Некоторые специальные случаи интерполяционной теоремы для интуиционистского исчисления предикатов. Чебышевский сборник. 2025;26(4):212-223. https://doi.org/10.22405/2226-8383-2025-26-4-212-223
For citation:
Cybulski D.A. Some special cases of the interpolation theorem for intuitionistic predicate calculus. Chebyshevskii Sbornik. 2025;26(4):212-223. (In Russ.) https://doi.org/10.22405/2226-8383-2025-26-4-212-223
Просмотров:
1
Послать статью по эл. почте 