On the Skolemization of existential quantifiers in intuitionistic logic
Publication date
2006
Editors
Advisors
Supervisors
DOI
Document Type
Article
Metadata
Show full item recordCollections
License
Abstract
In this paper an alternative Skolemization method is introduced that for a large class of formulas is sound and complete with respect to intuitionistic logic. This class extends the class of formulas for which standard Skolemization is sound and complete and includes all formulas in which all strong quantifiers are existential. The method makes use of an existence predicate first introduced by Dana Scott.
Keywords
Skolemization, eSkolemization, Herbrand’s theorem, intuitionistic logic, Kripke models, existence predicate
Citation
Iemhoff, R & Baaz, M 2006, 'On the Skolemization of existential quantifiers in intuitionistic logic', Annals of Pure and Applied Logic, vol. 142, no. (1-3), pp. 269-295.