Rosalie Iemhoff (Utrecht University) – Skolemization and quantifier shifts

The Skolemization method in first-order logic is a well-known translation on formulas that makes explicit the implicit functions hidden in quantifier combinations ∀∃. It is an important tool in certain areas in computer science but it also has intriguing properties from the viewpoint of logic. For classical logic, Skolemization is complete, meaning that a Skolemized formula is derivable if and only if its original is. But in intuitionistic and various other intermediate logics this is no longer the case.

In this talk I will give a short survey of some results about Skolemization in nonclassical logics. In particular, I will explain the necessary and sufficient condition for the completeness of Skolemization in intermediate logics, thereby showing how principles that express quantifier shifts over connectives determine whether in a given logic Skolemization is complete. The locally unsound proof systems introduced by Aguilera and Baaz play an important role in obtaining these results.

This is joint work with Matthias Baaz, Mariami Gamsakhurdia, and Raheleh Jalali.