Skolem is not constructive
(but sometimes it can be)
On what goes wrong when you try to eliminate quantifiers intuitionistically
proof theoryconstructive logicSkolemization works. That's the starting point — not a caveat, not a qualification. In classical first-order logic, it is a perfectly sound and complete procedure for eliminating existential quantifiers. It feels right. Given a formula with alternating quantifiers, you replace each existential one with a function symbol that witnesses the existential choice in terms of the universal variables above it. The prenex formula ∀x ∃y P(x,y) becomes ∀x P(x, f(x)), where f is a fresh Skolem function. The resulting formula is satisfiable if and only if the original is. It looks right because it is right.
So why doesn't it work constructively?
What goes wrong
In classical logic, ∀x ∃y P(x,y) being true means there exists a choice function picking a witness for each x. The Skolem function f simply names that function. The move is sound because classical logic is comfortable with non-constructive existence: "there is some y" doesn't require you to say which one, or how to find it.
Constructively, a proof of ∀x ∃y P(x,y) is a function that, given any x, produces a specific y together with a proof that P(x,y) holds. So far so good — that looks exactly like a Skolem function! But the catch comes when you try to preserve this under proof transformations. The issue is not just semantic but syntactic: Skolemization changes the formula, and intuitionistic logic is sensitive to the structure of formulas in ways classical logic is not.
More precisely, the classical equivalence
∀x ∃y P(x,y) ⟺ ∃f ∀x P(x, f(x))
fails constructively. The right-to-left direction is fine: given a function f and a proof that ∀x P(x, f(x)), you can obviously produce a witness for any given x. The left-to-right direction is the problem. Passing from a proof of the left side to an explicit choice function f in the metalanguage is precisely what the Axiom of Choice does. Intuitionistic logic does not have AC as a theorem, and for good reason: there are models — realizability models, sheaf models — where AC fails.
The philosophical point
There is something deeper going on here than a missing axiom. Classical logic treats truth as a property of statements independent of any proof. A statement is true or false, and if it's true there's nothing more to say about how or why. Constructive logic treats truth as tied to the existence of a construction — a proof, a program, a witness. When you Skolemize, you are packaging up the witnessing information into a function and pretending it was there all along. Classically, the function exists abstractly. Constructively, you need to hand it to me.
Sometimes it's constructively valid
Herbrand's theorem is itself a classical result, so it doesn't rescue constructive Skolemization directly. But its output is more honest than an abstract Skolem function: the theorem says that if a prenex formula is classically valid, then some finite disjunction of ground instances of its matrix is propositionally valid. You get actual explicit ground terms as witnesses — not an abstract choice function whose existence is merely asserted. That's a more tractable form of existence, even if the theorem that produces it is classical, and even if finding the right finite disjunction is in general only semi-decidable.
In dependent type theory (think Martin-Löf type theory or its descendants), the Skolem function is already present in the type of the proof. A term of type Πx:A. Σy:B. P(x,y) is literally a dependent function that maps each x to a pair (y, proof). You can project out the first component to get your Skolem function. No axiom needed — it's just projection. In the right foundational setting, Skolemization is not a trick but a triviality.
Realizability semantics enforces constructive content directly. In Kleene's number realizability, a proof of ∀x ∃y P(x,y) is realized by a computable function f such that for each x, f(x) is a realizer for P(x, f(x)). The Skolem function is literally the realizer — and it is required to be an actual computable function, not an abstract one. The semantics does the work that AC would otherwise do, by demanding computation.
Gödel's Dialectica interpretation (1958) makes witnessing explicit by translating intuitionistic arithmetic into a system of computable functionals. Interestingly, Gödel himself used Skolemization in arriving at the interpretation — he Skolemizes to extract the witnessing terms, then interprets those terms as computable functionals. (Troelstra's analysis in Gödel's Collected Works, vol. II makes this clear.) The point is not that Dialectica avoids Skolemization, but that it uses it in a setting where the Skolem functions are required to be computable — which is precisely the constructive content the interpretation is designed to capture.
The upshot
Skolemization is a classical procedure that packages up witnessing information into unnamed functions, relying on AC to justify the packaging. Constructively, you cannot take that shortcut — you have to carry the witnesses explicitly, which is exactly what dependent types, realizability semantics, and the Dialectica interpretation all do in their different ways.
The moral is not that Skolemization is wrong. It is right — classically. The constructive failure is informative precisely because the procedure is so well-motivated: it reveals that classical and constructive logic diverge not at some exotic corner case, but at the very heart of what it means to assert that something exists.
Related: Gödel's Dialectica interpretation (1958) · Herbrand's theorem · Martin-Löf type theory · Kleene realizability
No comments:
Post a Comment