Witnessed Models and Skolemization in Substructural Logics

Skolemization is an important ingredient of automated reasoning methods in (fragments of) first-order classical logic. A sentence (∀x̄)(∃y)ϕ(x̄, y) is satisfiable if and only if (∀x̄)ϕ(x̄, f(x̄)) is satisfiable, where f is a function symbol not occurring in ϕ. The satisfiability of a sentence in prenex form can therefore be reduced to the satisfiability of a universal sentence; Herbrand’s theorem then allows a further reduction to the satisfiability of a set of propositional formulas. In non-classical logics, the situation is not so clear. Consequence does not reduce to satisfiability, and, in general, sentences must be considered both as premises and as conclusions of consequences. Moreover, not all formulas are equivalent to prenex formulas. Skolemization can then be more carefully defined where strong occurrences of quantifiers in subformulas are replaced on the left, and weak occurrences on the right. However, satisfiability or validity, or, more generally, consequence, may not be preserved. Notably, in intuitionistic logic, formulas such as ¬¬(∀x)P (x) → (∀x)¬¬P (x) do not skolemize (see, e.g., [4]). For the consequence relation | = of a first-order non-classical logic, the goa