Специальные случаи интерполяционной теоремы для классического исчисления предикатов
https://doi.org/10.22405/2226-8383-2024-25-2-222-234
Аннотация
В статье доказываются специальные случаи интерполяционной теоремы для классического исчисления предикатов без функциональных символов и равенства. Накладывая ограничения на интерполируемые формулы, можно доказать существование интерполянта особого вида: универсального, экзистенциального, хорновского и универсального хорновского. Наиболее интересен случай универсального хорновского интерполянта: аксиомы многих алгебраических систем задаются универсальными хорновскими формулами. Ре-
зультаты, полученные в данной работе, могут быть полезны как с точки зрения теории доказательств, так и в приложениях, например, при решении задач искусственного интеллекта и разработке языков логического программирования. Статья написана в духе теории доказательств, основным инструментом для решения задачи служат секвенциальные исчисления и такие техники преобразования выводов, как обращение применений правил вывода, перестановка применений правил по С. К. Клини и прополка по В. П. Оревкову.
Статья состоит из введения, разбитой на 3 параграфа основной части и заключения.
Введение содержит краткий исторический обзор и обсуждение актуальности работы. В первом параграфе основной части вводятся необходимые определения и формулируется главный результат. Второй параграф посвящён описанию построенного В. П. Оревковым секвенциального исчисления KGL. Третий отведён доказательству основной теоремы. Заключение содержит обсуждение полученных результатов и краткий обзор перспектив дальнейшей работы.
Об авторе
Дмитрий Алексеевич Цибульский
Санкт-Петербургское отделение Математического института им. В. А. Стеклова РАН
Россия
Россия
аспирант
Список литературы
1. Craig W. Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem. // Jour. symbolic
2. logic, Vol. 22, P. 250-268.
3. Lynon R. C. An Interpolation Theorem in the Predicate Calculus. // Pacific jour. math., Vol.
4. , P. 129-142.
5. Тайцлин М. А. Реферат на ст. Линдона. // Jour. symbolic logic., Vol. 25, P. 273-274.
6. Henkin L. A. An Extension of the Craig–Lyndon Interpolation Theorem. // Ibid., Vol. 28, P.
7. -216.
8. Sch¨utte K. Der Interpolationssatz der intuitionistischen Pr¨adikaten-logik. // Math. Ann., Vol.
9. , P. 192-200.
10. Максимова Л. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые
11. многообразия псевдобулевых алгебр. // Алгебра и логика, т. 16:6, с. 643-681.
12. Maksimova L. On Variable Separation in Modal and Superintuitionistic Logics. // Studia
13. Logica, Vol. 55, P. 99-112.
14. Beth E. W. On Padoa’s Method in the Teory of Definition. // Ibid., Vol. 56, P. 330-339.
15. Robinson A. A Result of Consistency and It’s Application to the Theory of Definition. // Kon.
16. Ned. Akad., Amsterdam, Proc., Ser. A, Vol. 59, P. 47-58.
17. Kleene S. C. Mathematical Logic. // John Wiley & Sons, inc., 1967, New York, P. 394-441.
18. Мальцев А. И. Алгебраические системы. // Наука, 1970, Москва, с. 163-192.
19. Оревков В. П. Верхние оценки удлинения выводов при устранении сечений. // Записки
20. науч. семинаров ЛОМИ, т. 137, с. 87-98.
21. Оревков В. П. О гливенковских классах секвенций. // Труды ордена Ленина Мат. инсти-
22. тута им. Стеклова, т. 98, с. 131-154.
23. Ершов Ю.Л., Палютин Е. А. Математическая логика. // Наука, 1987, Москва, с. 209-214.
24. Gentzen G. Untersuchungen ¨uber das logische Schließen. I, II. // Math. Zeitschrift, Vol. 39, P. 176-210, 405-443.
25. Kleene S. C. Permutability of inferences in Gentzen’s caculi LK and LJ. // Memories of the
26. Am. math. society, Vol. 10, P. 1-26.
Рецензия
Для цитирования:
Цибульский Д.А. Специальные случаи интерполяционной теоремы для классического исчисления предикатов. Чебышевский сборник. 2024;25(2):222-234. https://doi.org/10.22405/2226-8383-2024-25-2-222-234
For citation:
Cybulski D.A. Special cases of the interpolation theorem for classical predicate calculus. Chebyshevskii Sbornik. 2024;25(2):222-234. (In Russ.) https://doi.org/10.22405/2226-8383-2024-25-2-222-234
Просмотров:
303
Послать статью по эл. почте 