Special cases of the interpolation theorem for classical predicate calculus

Abstract

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.