|
First order logic is extraordinarily messy, like most mathematical logic. It's a collection of symbols that don't easily translate into natural language thought patterns.
For example, take the following "theorem":
∀x ∀y ∃z: x + y < z
This could be translated as "For any x and y, we can find some number z which is greater than the sum of x and y." If you were to do this problem for a specific x and y, it would stand to reason that your choice of z would depend on the specific x and y. Skolemization is the process of formalizing the dependecy of existentials on the universals that precede them.
The basic rule for finding skolem functions is simple. Whenever you see an existential quantifier to the right of any universal quantifiers, there is a skolem function in every variable with a universal quantifier that determines the existential one. It's a good idea to keep the skolemization process in mind when dealing with predicate calculus because it makes the dependcies much easier to ferret out.
∀x ∀y ∃z: x + y < z
becomes
∃f(x, y) ∀x ∀y: x + y < f(x, y)
After doing this, it's easy enough to find a function that satisfies the condition. In the example, f(x, y) = x + y + 1 would satisfy, and the existence of such a function proves the proposition true.
The cool thing about all this is that the existential quantifier for the skolem function comes before all of the universals. This way, you can have standard forms for theorems in predicate calculus. There are many proofs regarding consistency and decideability which revolve around finding these normal forms. Dealing only with universals is indeed a good thing. | 
