Some special cases of the interpolation theorem for intuitionistic predicate calculus
https://doi.org/10.22405/2226-8383-2025-26-4-212-223
Abstract
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.
About the Author
Dmitry Alekseevich Cybulski
St. Petersburg Department of Steklov Mathematical Institute of the Russian Academy of Sciences
Russian Federation
Russian Federation
postgraduate student
References
1. Craig, W., 1957, “Linear Reasoning. A New Form of the Herbrand–Gentzen Theorem”, Journal of Symbolic Logic, 22, pp. 250–268.
2. Lyndon, R.C., 1959, “An Interpolation Theorem in the Predicate Calculus”, Pacific Journal of Mathematics, 9, pp. 129–142.
3. Sch¨utte, K., 1962, “Der Interpolationssatz der intuitionistischen Pr¨adikatenlogik”, Mathematische Annalen, 148, pp. 192–200.
4. 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.
5. Maksimova, L.L., 1995, “On Variable Separation in Modal and Superintuitionistic Logics”, Studia Logica, 55, pp. 99–112.
6. Beth, E.W., 1953, “On Padoa’s Method in the Theory of Definition”, Indagationes Mathematicae, 56, pp. 330–339.
7. 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.
8. Kleene, S.C., 1967, Mathematical Logic, New York: John Wiley & Sons, pp. 394–441.
9. Troelstra, A.S., and Schwichtenberg, H., 2000, Basic Proof Theory, Cambridge: Cambridge University Press, pp. 116–126.
10. Cybulski, D.A., 2024, “Special Cases of the Interpolation Theorem for Classical Predicate Calculus”, Chebyshevskii Sbornik, 25(2), pp. 222–234.
11. Orevkov, V.P., 1984, “Upper Bounds of Inference Elongation When Eliminating Cuts”, Zapiski Nauchnykh Seminarov POMI, 137, pp. 87–98.
12. Orevkov, V.P., 1976, “On Glivenko’s Classes of Sequents”, Trudy Matematicheskogo Instituta imeni V.A. Steklova, 98, pp. 131–154.
13. Ershov, Yu.L., and Paliutin, E.A., 1987, Mathematical Logic, Moscow: Nauka, pp. 209–214.
14. Gentzen, G., 1934, “Untersuchungen ¨uber das logische Schließen. I, II”, Mathematische Zeitschrift, 39, pp. 176–210, 405–443.
15. Kleene, S.C., 1952, “Permutability of Inferences in Gentzen’s Calculi LK and LJ”, Memoirs of the American Mathematical Society, 10, pp. 1–26.
16. Maehara, S., 1960, “On the Interpolation Theorem of Craig”, Sugaku, 12, pp. 235–237.
17. 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.
Review
For citations:
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
Views:
6
Email this article 