chebЧебышевский сборникChebyshevskii Sbornik2226-8383Tula State Lev Tolstoy Pedagogical University10.22405/2226-8383-2024-25-2-222-234cheb-1740Research ArticleСтатьиArticleСпециальные случаи интерполяционной теоремы для классического исчисления предикатовSpecial cases of the interpolation theorem for classical predicate calculusЦибульскийДмитрий АлексеевичCybulskiDmitry Alekseevich

аспирант

postgraduate student

cybulski@pdmi.ras.ruСанкт-Петербургское отделение Математического института им. В. А. Стеклова РАНРоссияSt. Petersburg Branch of the Steklov Mathematical Institute of the RASRussian Federation202419072024252222234Copyright © Цибульский Д.А., 20242024Цибульский Д.А.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/1740

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

The article proves special cases of the interpolation theorem for the classical predicate calculus without functional symbols and equality. By imposing restrictions on the interpolated formulas, it is possible to prove the existence of an interpolant of a special kind: universal, existential, Horn and universal Horn. The most interesting case is the universal Horn interpolant: the axioms of many algebraic systems are given by universal Horn formulas. The results obtainedin 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 inferencerules, 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 thesequential calculus KGL 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 theoremclassical predicate calculusuniversal interpolantHorn interpolantReferencesCraig W. Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem. // Jour. symbolicCraig, W. “Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem”, Jour. symboliclogic, Vol. 22, P. 250-268.logic, vol. 22, pp. 250-268.Lynon R. C. An Interpolation Theorem in the Predicate Calculus. // Pacific jour. math., Vol.Lynon, R. C. “An Interpolation Theorem in the Predicate Calculus”, Pacific jour. math., vol. 9,, P. 129-142.pp. 129-142.Тайцлин М. А. Реферат на ст. Линдона. // Jour. symbolic logic., Vol. 25, P. 273-274.Tayclin, M. A. “Abstract of Lyndon’s article”, Jour. symbolic logic., vol. 25, pp. 273-274.Henkin L. A. An Extension of the Craig–Lyndon Interpolation Theorem. // Ibid., Vol. 28, P.Henkin, L. A. “An Extension of the Craig–Lyndon Interpolation Theorem”, Ibid., vol. 28, pp.-216.-216.Sch¨utte K. Der Interpolationssatz der intuitionistischen Pr¨adikaten-logik. // Math. Ann., Vol.Sch¨utte, K. “Der Interpolationssatz der intuitionistischen Pr¨adikaten-logik”, Math. Ann., vol., P. 192-200., pp. 192-200.Максимова Л. Л. Теорема Крейга в суперинтуиционистских логиках и амальгамируемыеMaksimova, L. “Craig’s Theorem for Superintuitionistic Logics and Amalgamated Varieties ofмногообразия псевдобулевых алгебр. // Алгебра и логика, т. 16:6, с. 643-681.Pseudo-Boolean Algebras”, Algebra and Logic, vol. 16:6, pp. 643-681.Maksimova L. On Variable Separation in Modal and Superintuitionistic Logics. // StudiaMaksimova, L. “On Variable Separation in Modal and Superintuitionistic Logics”, Studia Logica, vol. 55, pp. 99-112.Logica, Vol. 55, P. 99-112.Beth, E.W. “On Padoa’s Method in the Teory of Definition. Ibid., vol. 56, pp. 330-339.Beth E. W. On Padoa’s Method in the Teory of Definition. // Ibid., Vol. 56, P. 330-339.Robinson, A. “A Result of Consistency and It’s Application to the Theory of Definition. Kon.Robinson A. A Result of Consistency and It’s Application to the Theory of Definition. // Kon.Ned. Akad., Amsterdam, Proc., Ser. A, vol. 59, pp. 47-58.Ned. Akad., Amsterdam, Proc., Ser. A, Vol. 59, P. 47-58.Kleene, S. C. “Mathematical Logic”, John Wiley & Sons, inc., 1967, New York, pp. 394-441.Kleene S. C. Mathematical Logic. // John Wiley & Sons, inc., 1967, New York, P. 394-441.Maltsev, A. I., 1970. “Algebraic Systems”, Nauka, Moscow, pp. 163-192.Мальцев А. И. Алгебраические системы. // Наука, 1970, Москва, с. 163-192.Orevkov, V.P. “Upper Bounds of Inference Elongation When Eliminating Cuts”, ZapiskiОревков В. П. Верхние оценки удлинения выводов при устранении сечений. // Запискиnauchnykh seminarov POMI, vol. 137, pp. 87-98.науч. семинаров ЛОМИ, т. 137, с. 87-98.Orevkov, V.P. “On Glivenko’s Classes of Sequents”, Trudy ordena Lenina MatematicheskogoОревков В. П. О гливенковских классах секвенций. // Труды ордена Ленина Мат. инсти-Instituta Steklova, vol. 98, pp. 131-154.тута им. Стеклова, т. 98, с. 131-154.Ershov, Yu. L., Paliutin, E. A., 1987. “Mathematical Logic”, Nauka, Moskov, pp. 209-214.Ершов Ю.Л., Палютин Е. А. Математическая логика. // Наука, 1987, Москва, с. 209-214.Gentzen, G. “Untersuchungen ¨uber das logische Schließen. I, II”, Math. Zeitschrift, vol. 39, pp. 176-210, 405-443.Gentzen G. Untersuchungen ¨uber das logische Schließen. I, II. // Math. Zeitschrift, Vol. 39, P. 176-210, 405-443.Kleene, S. C. “Permutability of inferences in Gentzen’s caculi LK and LJ”, Memories of the Am. math. society, vol. 10, pp. 1-26.Kleene S. C. Permutability of inferences in Gentzen’s caculi LK and LJ. // Memories of theKleene S. C. Permutability of inferences in Gentzen’s caculi LK and LJ. // Memories of theAm. math. society, Vol. 10, P. 1-26.Am. math. society, Vol. 10, P. 1-26.

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