Skolemization in Intuitionistic Logic
Utrecht University
Slides
Abstract:
In contrast to classical logic, Skolemization is in intuitionistic logic, and
many other intermediate logics, not complete. The Skolem class of a logic
consists of those formulas for which derivability is equivalent to the derivability
of their Skolemization. Thus the Skolem class of classical logic consists of all
formulas, but for intuitionistic logic it does not. We show that for a large
class of intermediate logics, including intuitionistic logic, all prenex formulas
as well as certain propositional combinations of such formulas, belong to the
Skolem class of the logic. This implies that the usual counter examples to
Skolemization for intermediate logics, such as the formula for constant domains
or the existential double negation shift, are in some sense the simplest formulas
that do not belong to its Skolem class. We furthermore discuss the possibility
of alternative Skolemization methods and show that under mild conditions on
such translations one can prove that, like Skolemization, they are not complete
for intuitionistic logic.