A language has two constants {a, b} and one binary function symbol f. Which of the following is a member of the Herbrand universe of this language?
A∀x P(x) → Q(x) (a first-order formula)
Bf(a, f(b, a)) (a ground term built from constants and function applications)
Cx (a free variable)
DP(a) (a ground atom — a formula, not a term)
The Herbrand universe contains ground terms — expressions built from constants and function symbols with no variables remaining. f(a, f(b, a)) is a valid ground term: f applied to the constant a and to the ground term f(b, a). Formulas like ∀x P(x) → Q(x) and ground atoms like P(a) are not terms — they are logical formulas. Variables like x are not ground terms because they are not closed. The Herbrand universe is a syntactic object: the set of all term-level expressions that can be written using the language's constants and function symbols.
Question 2 Multiple Choice
Herbrand's theorem is most significant for automated theorem proving because it allows:
AProof that first-order logic is decidable by reducing satisfiability checking to finite propositional logic
BSatisfiability checking to be restricted to Herbrand interpretations — a concrete, computable domain — rather than quantifying over all possible abstract domains of any cardinality
CA polynomial-time algorithm for determining whether any set of clauses is satisfiable
DEvery consistent first-order theory to be represented by a single canonical Herbrand model
Herbrand's theorem does not make first-order logic decidable (it remains undecidable). What it achieves is a reduction in the scope of search: instead of checking satisfiability over all possible interpretations with all possible domains (an uncountable space), you only need to check Herbrand interpretations, where the domain is fixed as the set of ground terms. This makes the search concrete and computable, even though the Herbrand universe may be infinite. Resolution-based provers exploit this by working directly with ground instances.
Question 3 True / False
The Herbrand universe of a language with at least one function symbol of arity greater than zero is always infinite, because applying the function symbol to ground terms generates new ground terms without bound.
TTrue
FFalse
Answer: True
If the language has a constant a and a unary function f, then f(a), f(f(a)), f(f(f(a))), … are all distinct ground terms, generating an infinite Herbrand universe. Only when the language has no function symbols of positive arity — only constants — is the Herbrand universe finite (it is just the set of constants). This is why automated theorem provers working with Herbrand models must manage the potentially infinite generation of ground instances with careful heuristics.
Question 4 True / False
In a Herbrand interpretation, the predicate symbols are interpreted as themselves syntactically, just as function symbols are — so P(a) is 'true' in most Herbrand interpretation that contains the constant a.
TTrue
FFalse
Answer: False
Function symbols are interpreted as themselves (f(t) maps to the ground term f(t)), but predicate symbols are not. The interpretation of predicates is the only free choice in a Herbrand model: for each predicate P, you choose which tuples of ground terms satisfy P. Different Herbrand interpretations disagree only on which ground atoms are true — this is what makes the class of Herbrand interpretations non-trivial. P(a) is true in some Herbrand interpretations and false in others, depending on whether the tuple (a) is included in P's extension.
Question 5 Short Answer
Why does satisfiability over all possible first-order interpretations (with arbitrary domains) reduce to satisfiability over just Herbrand interpretations? What is the key insight that makes this reduction valid?
Think about your answer, then reveal below.
Model answer: The key insight is that if a formula Φ is satisfiable at all, it has a Herbrand model. Given any satisfying interpretation M with domain D, you can construct a Herbrand interpretation H that also satisfies Φ: map each element of D to some ground term that 'names' it (via the terms that witness existential quantifiers), and define predicate extensions in H to match M's truth values on those terms. Because this mapping preserves satisfaction, H witnesses satisfiability just as M does. So unsatisfiability over all interpretations equals unsatisfiability over Herbrand interpretations — and the latter can be checked by examining finite sets of ground instances.
If this reduction failed — if some formulas were satisfiable only in non-Herbrand domains — then automated theorem provers based on resolution and ground instances would be incomplete. The reduction is what gives Herbrand-based methods their soundness and (semi-)completeness: a prover that systematically generates ground instances and applies resolution will eventually find a contradiction if and only if the formula is unsatisfiable.