Special cases of the interpolation theorem for classical predicate calculus

D. A. Cybulski

Čebyševskij sbornik, Tome 25 (2024) no. 2, pp. 222-234.

Résumé

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 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 sequential 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.

Détail

Keywords: interpolation theorem, classical predicate calculus, universal interpolant, Horn interpolant.

Bibliographie

[1] Craig, W., “Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem”, Jour. symbolic logic, 22, 250–268 | DOI | MR | Zbl

[2] Lynon, R. C., “An Interpolation Theorem in the Predicate Calculus”, Pacific jour. math., 9, 129–142 | DOI | MR

[3] Tayclin, M. A., “Abstract of Lyndon's article”, Jour. symbolic logic, 25, 273–274 | DOI | MR

[4] Henkin L. A., “An Extension of the Craig–Lyndon Interpolation Theorem”, Jour. symbolic logic, 28, 201–216 | DOI | MR | Zbl

[5] Schütte K., “Der Interpolationssatz der intuitionistischen Prädikaten-logik”, Math. Ann., 148, 192–200 | DOI | MR | Zbl

[6] Maksimova, L., “Craig's Theorem for Superintuitionistic Logics and Amalgamated Varieties of Pseudo-Boolean Algebras”, Algebra and Logic, 16:6, 643–681 | MR | Zbl

[7] Maksimova, L., “On Variable Separation in Modal and Superintuitionistic Logics”, Studia Logica, 55, 99–112 | DOI | MR | Zbl

[8] Beth E. W., “On Padoa's Method in the Teory of Definition”, Studia Logica, 56, 330–339 | MR | Zbl

[9] Robinson A., “A Result of Consistency and It's Application to the Theory of Definition”, Kon. Ned. Akad., Amsterdam, Proc., Ser. A, 59, 47–58 | MR | Zbl

[10] Kleene S. C., Mathematical Logic, John Wiley Sons, inc, New York, 1967, 394–441 | MR

[11] Maltsev, A. I., Algebraic Systems, Nauka, M., 1970, 163–192

[12] Orevkov, V. P., “Upper Bounds of Inference Elongation When Eliminating Cuts”, Zapiski nauchnykh seminarov POMI, 137, 87–98 | MR | Zbl

[13] Orevkov, V. P., “On Glivenko's Classes of Sequents”, Trudy ordena Lenina Matematicheskogo Instituta Steklova, 98, 1968, 131–154 | MR | Zbl

[14] Ershov, Yu. L., Paliutin, E. A., Mathematical Logic, Nauka, M., 1987, 209–214 | MR

[15] Gentzen G., “Untersuchungen über das logische Schließen. I, II”, Math. Zeitschrift, 39, 176–210 | DOI | MR | Zbl

[16] Kleene S. C., “Permutability of inferences in Gentzen's caculi LK and LJ”, Memories of the Am. math. society, 10, 1–26 | MR | Zbl