The Skolemization of existential quantifiers in intuitionistic logic (Q2503404)

Skolemization, together with Herbrand's theorem, is one of the fundamental methods to connect a predicate logic with its propositional base, and is applied in several problems such as decidability, automated theorem proving, and so on. In classical logic, as is well-known, any formula can be Skolemized preserving provability. As for intuitionistic logic, however, the method does not work for all formulas but only for those which are characterized by G. E. Mints. In this paper, an alternative method of Skolemization, called eSkolemization, is proposed. Roughly speaking, it restricts the Skolem function employed for a strong quantification so as to range over ``existing'' terms to be defined thus by means of the existence predicate introduced by D. S. Scott. The method covers much more formulas than the standard one; for example, all formulas in which all strong quantifiers are existential. The authors first provide a Gentzen system, called LJE, for the logic, extended from the in\-tui\-tio\-nistic one by adding the existence predicate where the quantifiers are relativized to existing terms by making use of the predicate, and then prove the soundness and completeness of LJE with respect to a Kripke semantics designed naturally. The main result on eSkolemization is proved in LJE according to the Kripke semantics, and applied to Gentzen's original LJ as well via certain conservativeness of LJE with respect to LJ. The paper includes also some observations on the properties of LJE; cut-elimination, interpolation, etc., for instance.