On Skolemization in constructive theories (2008)

Titel On Skolemization in constructive theories
Gepubliceerd in Logic Group Preprint Series, Vol. 256.
Auteur Baaz, Matthias; Iemhoff, R.
Datum 2008-03-20
Taal Engels
Type Preprint
Samenvatting 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.
Persistent Identifier URN:NBN:NL:UI:10-1874-26723
Metadata XML
Bron Universiteit Utrecht

Ga terug naar de inhoud
Ga terug naar de site navigatie