A theory T contains the sentence ∃x∃y R(x, y). When we Skolemize this, we introduce two function symbols. Which of the following correctly captures the dependency structure?
ATwo 0-ary constants c₁ and c₂, because neither quantifier has free variables
BA constant c for x and a unary function g(c) for y, because y's witness may depend on the choice of x
CTwo unary functions f(x) and g(y), because each witness depends on the other
DA single binary function f(x, y) covering both quantifiers simultaneously
The outer ∃x has no free variables, so its witness is a constant c. But the inner ∃y is within the scope of x, so y's witness may depend on which x was chosen — it needs a unary function g(x). The Skolem form is R(c, g(c)). Option A misses the dependency; options C and D misrepresent how Skolemization works one quantifier at a time.
Question 2 Multiple Choice
You have a model M of a Skolemized theory T* and a countable set A ⊆ M. You form the Skolem hull of A. What does this give you?
AThe smallest substructure of M containing A, but not necessarily an elementary substructure
BThe smallest elementary substructure of M containing A
CA copy of A with all existential witnesses added, which may be larger than M
DThe unique prime model of T* over A
The Skolem hull — closing A under all Skolem functions repeatedly — yields the smallest *elementary* substructure containing A. Elementary substructure means it satisfies exactly the same first-order sentences as M (when parameters from it are used). The key is that every ∃-witness in M that M 'uses' for elements of the hull is already named by a Skolem term, so truth is preserved. Option A is wrong: the hull is more than a plain substructure.
Question 3 True / False
Skolemizing a theory T to get T* can change which sentences are provable in the original language of T.
TTrue
FFalse
Answer: False
Skolemization is a conservative extension: T* proves every sentence of T's original language that T proves, and nothing more. Any model of T can be expanded to a model of T* by choosing witnesses for the Skolem functions, and any model of T* restricts to a model of T. The theories are equi-satisfiable, and the Skolem functions add no new consequences in the original language.
Question 4 True / False
Herbrand's theorem establishes that a first-order formula is unsatisfiable if and only if a finite set of its ground instances — evaluated on Herbrand terms built from constants and Skolem functions — is propositionally unsatisfiable.
TTrue
FFalse
Answer: True
This is precisely Herbrand's theorem. Skolem functions are the key bridge: they replace existential quantifiers (which require witnesses that vary by context) with explicit functional terms that can be instantiated to ground terms. This reduces the first-order question to a propositional one over a concrete, enumerable set of ground instances — the foundation of resolution-based automated theorem proving.
Question 5 Short Answer
Why does closing a countable set A under all Skolem functions yield an elementary substructure of M, rather than merely a substructure?
Think about your answer, then reveal below.
Model answer: Because every existential formula ∃x φ(x, ā) that is true in M for parameters ā from the hull already has its witness named by the corresponding Skolem term f_φ(ā), which is in the hull by construction. When checking whether ∃x φ(x, ā) holds in the hull, we find the witness f_φ(ā) right there — so the hull satisfies every existential (and therefore every first-order) sentence that M satisfies with parameters from the hull. This is Tarski's criterion for elementary substructure.
The contrast with a plain substructure is crucial. A plain substructure just requires closure under functions and relations; it might fail to satisfy ∃x φ(x, ā) if the witness in M is outside the substructure. The Skolem hull specifically ensures witnesses are always internal, which is exactly what elementary substructure requires.