A signature contains exactly one constant symbol (a) and one unary function symbol (f). How many ground terms does this signature generate?
A1 — only the constant a
B2 — the constant a and the term f(a)
CFinitely many — up to some fixed nesting depth determined by the signature
DInfinitely many — a, f(a), f(f(a)), f(f(f(a))), and so on without bound
Ground terms are built recursively: every constant is a ground term, and applying a function symbol to ground terms produces a new ground term. With one constant a and one unary function f, we can always nest one more level: a, f(a), f(f(a)), f(f(f(a))), .... There is no upper bound on nesting depth, so infinitely many ground terms are generated from just two symbols. This surprises students who expect a finite signature to yield a finite domain.
Question 2 Multiple Choice
Consider the formula ∀x P(x, a) where a is a constant and P is a binary predicate. Is this formula ground?
AYes — the quantifier ∀x binds every occurrence of x, so the formula is closed and therefore ground
BNo — the bound variable x still appears in the atom P(x, a), making that atom non-ground, even though the formula has no free variables
CYes — since a is a constant and x is universally quantified, the formula makes assertions about specific objects
DNo — only atomic formulas (without any connectives or quantifiers) can be ground
Being closed (no free variables) and being ground are different properties. ∀x P(x, a) is closed because x is bound by ∀ — but x still syntactically appears in the atom P(x, a), making that atom non-ground. Ground formulas require that every term appearing in any atom contains no variables at all, not even bound ones. A ground formula has only constants and function-symbols-applied-to-constants, never any variable symbols.
Question 3 True / False
A ground formula is always a closed formula (no free variables), but a closed formula is not always a ground formula.
TTrue
FFalse
Answer: True
Every ground formula has no variables of any kind, so trivially no free variables — it is closed. But a closed formula like ∀x P(x, a) has no free variables yet contains the bound variable x, making its internal atom non-ground. The set of ground formulas is a proper subset of closed formulas.
Question 4 True / False
Ground terms can mainly be formed from constant symbols alone — applying function symbols to constants does not yield a ground term.
TTrue
FFalse
Answer: False
Function symbols applied to ground terms produce ground terms. For example, if a is a constant and f is a binary function symbol, then f(a, a) is a ground term because it contains no variables. The definition of ground is variable-free, not function-free. Constants are the base cases; function symbols applied to ground terms are the inductive cases.
Question 5 Short Answer
Explain why the Herbrand universe relies on ground terms, and what Herbrand's theorem allows us to conclude about first-order satisfiability.
Think about your answer, then reveal below.
Model answer: The Herbrand universe consists of all ground terms constructible from the signature — the specific named objects a formula can talk about. Herbrand's theorem says that a set of first-order clauses is unsatisfiable if and only if some finite set of its ground instances (propositional formulas obtained by substituting ground terms for variables) is unsatisfiable. This reduces first-order reasoning to propositional reasoning over concrete objects.
The power of this reduction is computational: instead of verifying a formula against all possible domains and interpretations (which could be uncountably infinite), we only need to check the Herbrand universe — the objects the formula itself generates. Herbrand's theorem guarantees that if a contradiction exists, it can be witnessed by a finite set of ground instances, which is why automated theorem provers can systematically enumerate and check ground instances until they find a refutation.