chebЧебышевский сборникChebyshevskii Sbornik2226-8383Tula State Lev Tolstoy Pedagogical University10.22405/2226-8383-2025-26-4-212-223cheb-2079Research ArticleСтатьиArticleНекоторые специальные случаи интерполяционной теоремы для интуиционистского исчисления предикатовSome special cases of the interpolation theorem for intuitionistic predicate calculusЦибульскийДмитрий АлексеевичCybulskiDmitry Alekseevich

аспирант

postgraduate student

cybulski@pdmi.ras.ruСанкт-Петербургское отделение Математического института имени В. А. Стеклова РАНРоссияSt. Petersburg Department of Steklov Mathematical Institute of the Russian Academy of SciencesRussian Federation202529122025264212223Copyright © Цибульский Д.А., 20252025Цибульский Д.А.Cybulski D.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.chebsbornik.ru/jour/article/view/2079

Заметка посвящена доказательству некоторых вариантов интерполяционной теоремы для интуиционистского исчисления предикатов без функциональных символов и равенства с интерполянтом специального вида. Наиболее интересен случай универсального хорновского интерполянта: аксиомы многих алгебраических систем задаются универсальными хорновскими формулами. Результаты, полученные в данной работе, могут быть полезны как с точки зрения теории доказательств, так и в приложениях, например, при решении задач искусственного интеллекта и разработке языков логического программирования. Заметка написана в духе теории доказательств, основным инструментом для решения задачислужат секвенциальные исчисления и такие техники преобразования выводов, как обращение применений правил вывода, перестановка применений правил по С. К. Клини и прополка по В. П. Оревкову.Заметка состоит из введения, разбитой на 3 параграфа основной части и заключения. Введение содержит краткий исторический обзор и обсуждение актуальности работы. Впервом параграфе основной части вводятся необходимые определения и формулируется главный результат. Второй параграф посвящён описанию построенного В. П. Оревковым секвенциального варианта интуиционистского исчисления предикатов IGL. Третий отведён доказательству основной теоремы. Заключение содержит обсуждение полученных результатов и краткий обзор перспектив дальнейшей работы.

The article proves some variants of the interpolation theorem for the intuitionistic predicate calculus without functional symbols and equality with a special-form interpolant. The most interesting case is the universal Horn interpolant: the axioms of many algebraic systems are given by universal Horn formulas. The results obtained in this work can be useful both from the point of view of proof theory and in applications, for example, when solving problems of artificial intelligence and developing logical programming languages. The article is written in the spirit of proof theory, the main tools are sequential calculus and such techniques for proof transforming as reversing the applications of inference rules, rearranging the applications of rules according to S. K. Kleene and weeding according to V. P. Orevkov.The article consists of an introduction, the main part divided into 3 paragraphs, and a conclusion. The introduction contains a brief historical overview and discussion of the relevance of the work. In the first paragraph of the main part, the necessary definitions are introduced and the main result is formulated. The second paragraph is devoted to the description of the version of sequent intuitionistic predicate calculus IGL constructed by V. P. Orevkov. The third one is devoted to the proof of the main theorem. The conclusion contains a discussion of the results obtained and a brief overview of the prospects for further work.

интерполяционная теоремаинтуиционистское исчисление предикатовуниверсальный интерполянтхорновский интерполянт.interpolation theoremintuitionistic predicate calculusuniversal interpolantHorn interpolant.ReferencesCraig W. Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem // Journal of Symbolic Logic. — 1957. — Vol. 22. — P. 250–268.Craig, W., 1957, “Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem”, Journal of Symbolic Logic, 22, pp. 250–268.Lyndon R. C. An Interpolation Theorem in the Predicate Calculus // Pacific Journal of Mathematics. — 1959. — Vol. 9. — P. 129–142.Lyndon, R.C., 1959, “An Interpolation Theorem in the Predicate Calculus”, Pacific Journal of Mathematics, 9, pp. 129–142.Sch¨utte K. Der Interpolationssatz der intuitionistischen Pr¨adikatenlogik // Mathematische Annalen. — 1962. — Vol. 148. — P. 192–200.Sch¨utte, K., 1962, “Der Interpolationssatz der intuitionistischen Pr¨adikatenlogik”, Mathematische Annalen, 148, pp. 192–200.Максимова Л. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемые многообразия псевдобулевых алгебр // Алгебра и логика. — 1977. — Т. 16, № 6. — С. 643–681.Maksimova, L.L., 1977, “Craig’s Theorem for Superintuitionistic Logics and Amalgamated Varieties of Pseudo-Boolean Algebras”, Algebra and Logic, 16(6), pp. 643–681.Maksimova L. On Variable Separation in Modal and Superintuitionistic Logics // Studia Logica. — 1995. — Vol. 55. — P. 99–112.Maksimova, L.L., 1995, “On Variable Separation in Modal and Superintuitionistic Logics”, Studia Logica, 55, pp. 99–112.Beth E. W. On Padoa’s Method in the Theory of Definition // Indagationes Mathematicae. — 1953. — Vol. 56. — P. 330–339.Beth, E.W., 1953, “On Padoa’s Method in the Theory of Definition”, Indagationes Mathematicae, 56, pp. 330–339.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.Robinson, A., 1956, “A Result of Consistency and Its Application to the Theory of Definition”, Koninklijke Nederlandse Akademie van Wetenschappen. Proceedings. Series A, 59, pp. 47–58.Kleene S. C. Mathematical Logic. — New York: John Wiley & Sons, 1967. — 394–441 p.Kleene, S.C., 1967, Mathematical Logic, New York: John Wiley & Sons, pp. 394–441.Troelstra A. S., Schwichtenberg H. Basic Proof Theory. — Cambridge: Cambridge University Press, 2000. — 116–126 p.Troelstra, A.S., and Schwichtenberg, H., 2000, Basic Proof Theory, Cambridge: Cambridge University Press, pp. 116–126.Цибульский Д. А. Специальные случаи интерполяционной теоремы для классического исчисления предикатов // Чебышевский сборник. — 2024. — Т. 25, № 2. — С. 222–234.Cybulski, D.A., 2024, “Special Cases of the Interpolation Theorem for Classical Predicate Calculus”, Chebyshevskii Sbornik, 25(2), pp. 222–234.Оревков В. П. Верхние оценки удлинения выводов при устранении сечений // Записки научных семинаров ЛОМИ. — 1984. — Т. 137. — С. 87–98.Orevkov, V.P., 1984, “Upper Bounds of Inference Elongation When Eliminating Cuts”, Zapiski Nauchnykh Seminarov POMI, 137, pp. 87–98.Оревков В. П. О гливенковских классах секвенций // Труды Математического института имени В. А. Стеклова. — 1976. — Т. 98. — С. 131–154.Orevkov, V.P., 1976, “On Glivenko’s Classes of Sequents”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 98, pp. 131–154.Ершов Ю. Л., Палютин Е. А. Математическая логика. — М.: Наука, 1987. — 209–214 с.Ershov, Yu.L., and Paliutin, E.A., 1987, Mathematical Logic, Moscow: Nauka, pp. 209–214.Gentzen G. Untersuchungen ¨uber das logische Schließen. I, II // Mathematische Zeitschrift. — 1934. — Vol. 39. — P. 176–210, 405–443.Gentzen, G., 1934, “Untersuchungen ¨uber das logische Schließen. I, II”, Mathematische Zeitschrift, 39, pp. 176–210, 405–443.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.Kleene, S.C., 1952, “Permutability of Inferences in Gentzen’s Calculi LK and LJ”, Memoirs of the American Mathematical Society, 10, pp. 1–26.Maehara S. On the Interpolation Theorem of Craig // Sugaku. — 1960. — Vol. 12. — P. 235–237.Maehara, S., 1960, “On the Interpolation Theorem of Craig”, Sugaku, 12, pp. 235–237.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.Maehara, S., and Takeuti, G., 1961, “A Formal System of First-order Predicate Calculus With Infinitely Long Expressions”, Journal of the Mathematical Society of Japan, 13, pp. 357–370.

The authors declare that there are no conflicts of interest present.