Skolem is not constructive

Skolem is not constructive (but sometimes it can be) On what goes wrong when you try to eliminate quantifiers intuitionistically proof theory constructive logic Skolemization 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 th