| authors | Iemhoff, R. |
| source | Logic Group Preprint Series, Volume: 277 (2009), pp. 1-23 |
| full text | [Full text]
|
| publisher | Department of Philosophy, Utrecht University |
| URL publisher | [Website publisher]
|
| document type | Preprint |
| disciplines | Wijsbegeerte |
| 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. |
| keywords | skolemization, eskolemization, Herbrand's theorem, constructive theories, intuitionistic logic, decidability |
| ISSN | 0929-0710 |
