38th Logic Seminar
Skolemization and Herbrand's theorem in constructive theories
Rosalie Iemhoff

Department of Philosophy
Utrecht University

2012-11-08, 14-16

Seminar room of the RCIS, 3. floor

The Skolemization method is based on the intuition that proving a universally quantified statement is the same as proving the statement for an arbitrary object.

Herbrand's theorem builds on this insight by showing that existentially quantified statements are equi-consistent with propositional ones that can be obtained from the original statement in a canonical way. In the setting of constructive theories these methods fail to be complete. In the talk I will present variants of Skolemization that are sound and complete for constructive theories, and explain how they easily imply an analogue of Herbrand's theorem. After that I will discuss the implications of these results for various well-known constructive theories.

Contact Person

Norbert Preining