Skolemization in Intuitionistic Logic

Skolemization is the familiar procedure by which you replace strong quantifiers in a formula by function symbols in such a way that A is provable iff AS is provable. This doesn’t work in intuitionistic logic: the “only if” works, but the “if” doesn’t. E.g., ¬¬(A(c) ∨ ¬ A(c)) is provable intuitionistically, but not ¬¬(∀x)(A(x) ∨ ¬ A(x)). (If you also have =, it doesn’t even work for prenex formulas.) Rosalie Iemhoff is reporting on joint work with Matthias Baaz on new results on how to get Skolemization to work in constructive extensions of intuitionistic logic. The key is to add an existence predicate to intuitionistic (a logic proposed by Dana Scott1). Rosalie and Matthias showed that there’s a way to Skolemize strong existential quantifiers in this system.2 Now they have some ideas on how to also deal with strong universal quantifiers.

1 Dana S. Scott, Identity and existence in intuitionistic logic. In: Fourman et al., (ed.), Applications of Sheaves , LNM 753 (Springer, 1979) 660–696.
2 Matthias Baaz and Rosalie Iemhoff. On the Skolemization of existential quantifiers in intuitionistic logic. Annals of Pure and Applied Logic 142 (2006) 269-295.

Leave a Reply

Your email address will not be published. Required fields are marked *