Axiomatization of a Skolem function in intuitionistic logic

MaRDI QIDQ2702564zbMATH OpenFDO

Authors G. E. Mints

Publication date 24 July 2001

zbMATH Keywords

axiomatization of the Skolem extension of intuitionistic logic with equalitycompleteness proofskolemization

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Proof theory in general (including proof-theoretic semantics) (03F03)

Review text

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

Recommendations

• The Skolemization of existential quantifiers in intuitionistic logic
• Truth Definitions, Skolem Functions and Axiomatic Set Theory
• Eskolemization in intuitionistic logic
• Skolemization for Substructural Logics
• On Skolemization in constructive theories

Cited in

(14)

• The Skolemization of prenex formulas in intermediate logics
• The Skolemization of existential quantifiers in intuitionistic logic
• Skolemization in simple type theory: the logical and the theoretical points of view
• Eskolemization in intuitionistic logic
• Algebraic theories with definable Skolem functions
• scientific article; zbMATH DE number 31268 (Why is no real title available?)
• Truth Definitions, Skolem Functions and Axiomatic Set Theory
• Three faces of natural deduction
• Skolem functions in non-classical logics
• Skolemization in intermediate logics with the finite model property
• Skolem’s Theorem in Coherent Logic
• Constructibility and Geometry
• The eskolemization of universal quantifiers
• Gentzen calculi for the existence predicate

This page was built for publication: Axiomatization of a Skolem function in intuitionistic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2702564)