On Skolemization in constructive theories

Journal of Symbolic Logic 73 (3):969-998 (2008)
  Copy   BIBTEX

Abstract

In this paper a method for the replacement, in formulas, of strong quantifiers by functions is introduced that can be considered as an alternative to Skolemization in the setting of constructive theories. A constructive extension of intuitionistic predicate logic that captures the notions of preorder and existence is introduced and the method, orderization, is shown to be sound and complete with respect to this logic. This implies an analogue of Herbrand's theorem for intuitionistic logic. The orderization method is applied to the constructive theories of equality and groups

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 99,362

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2010-09-12

Downloads
45 (#398,184)

6 months
6 (#720,360)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Rosalie Iemhoff
Utrecht University

Citations of this work

Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
The eskolemization of universal quantifiers.Rosalie Iemhoff - 2010 - Annals of Pure and Applied Logic 162 (3):201-212.

Add more citations

References found in this work

Add more references