| Title | The eskolemization of universal quantifiers |
|---|---|
| Published in | Logic Group Preprint Series, Vol. 277, p.1-23. ISSN 0929-0710. |
| Author | Iemhoff, R. |
| Date | 2009-06 |
| 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. |
| Publication | http://igitur-archive.library.uu.nl/ph/2009-0623-200505/UUin... |
| 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