A formula of first-order logic is in Skolem normal form if its prenex normal form has only universal quantifiers. A formula can be Skolemized, that is have its existential quantifiers eliminated to produce an equisatisfiable formula to the original.
The essence of skolemization is the observation that if a formula in the form
is satisfiable in some model, then there must be some point in the model for every
Skolem also pointed out that a consequence of the Löwenheim-Skolem theorem is what is now known as Skolem's paradox: If Zermelo's axioms are consistent, then they must be satisfiable within a countable domain, even though they prove the existence of uncountable sets.
Skolem distrusted the completed infinite and was one of the founders of finitism in mathematics.
Skolem (1923) sets out his primitive recursive arithmetic, a very early contribution to the theory of computable functions, as a means of avoiding the so-called paradoxes of the infinite.
Feeds |
Contact