On Skolemization... again
Valeria (noreply@blogger.com)
Skolemization and Why It Fails Constructively There is a standard move in classical logic that feels so innocent. You take a formula with existential quantifiers depending on universals, and you replace those existential witnesses with function symbols. You eliminate existential quantifiers altogether, at the price of expanding the language. The result is equisatisfiable, often easier to manipulate, and forms the backbone of many proof procedures. The move is called Skolemization. In classical l