The eskolemization of universal quantifiers (2009)

Title The eskolemization of universal quantifiers
Published in Logic Group Preprint Series, Vol. 277, p.1-. ISSN 0929-0710.
Author Iemhoff, R.
Date 2009-06
Reference(s) skolemization, eskolemization, Herbrand's theorem, constructive theories, intuitionistic logic, decidability
Language English
Type Preprint
Publisher Department of Philosophy, Utrecht University
Abstract This paper is a sequel to the papers [4,6] in which an alternative skolemization method called ekolemization was introduced that, when applied to the strong existential quantifiers in a formula, is sound and complete for constructive theories. Based on that method an analogue of Herbrand’s theorem was proved to hold as well. In this paper we extend the method to universal quantifiers and show that for theories satisfying the witness property the method is sound and complete for all formulas. We prove a Herbrand theorem and, as an example, apply the method to several constructive theories. We show that for the theories with decidable quantifier-free fragment, also the strong existential quantifier fragment is decidable.
Persistent Identifier URN:NBN:NL:UI:10-1874-34087
Metadata XML
Repository Utrecht University

Go to page top
Go back to contents
Go back to site navigation