Axiomatization of a Skolem function in intuitionistic logic (Q2702564)

Skolemization is traditionally used to simplify the form and clarify the meaning of axioms. In the case of classical logic it allows to eliminate existential quantifiers and put all axioms into a universal form. In the case of intuitionistic logic skolemization is desirable, particularly in view of the possibility to extract programs from intuitionistic proofs. A deep investigation of skolemization in intuitionistic logic for non-prenex formulas was done by the same author [\textit{G. Mints}, Tr. Mat. Inst. Steklova 121, 67-99 (1972; Zbl 0282.02007); translation in Proc. Steklov Inst. Math. 121 (1972), 73-109 (1974; Zbl 0286.02030)]. \textit{C. Smorynski} [J. Symb. Log. 42, 530-544 (1977; Zbl 0381.03046)] presented an axiomatization of the Skolem extension of intuitionistic logic with equality with the corresponding completeness proof based on transformations of Kripke models. In this paper the author presents a completeness proof for Smorynski's axiomatization, based on a simple transformation of derivations. This proof can be easily simplified into a completeness proof for the ordinary skolemization for intuitionistic logic without equality.NEWLINENEWLINEFor the entire collection see [Zbl 0939.00009].