Jacques Herbrand

Jacques Herbrand

Mathematician, 1908–1931. Study focus: ground instances, witnesses, and why a finite proof may require an unbounded search.

Herbrand's work connects first-order reasoning with finite propositional reasoning. The important idea is not that every first-order question becomes one immediately available finite truth table. Rather, an unsatisfiable problem in the appropriate form has a finite set of ground instances witnessing the contradiction. Finding those instances is the search problem.

Historical setting

Herbrand entered the École Normale Supérieure in 1925. His thesis work on proof theory was published in 1930. He also worked in algebra and number theory and visited von Neumann in Berlin, Artin in Hamburg, and Noether in Göttingen. He died in a climbing accident in the Alps in July 1931. The surviving work matters without speculation about what he would have invented had he lived longer. MacTutor biography, original thesis record

The theorem now taught in automated reasoning has several formulations and a history of refinement. The original proof contained an issue later identified by logicians. A modern teaching statement should identify its assumptions rather than repeat an unqualified claim that Herbrand's original thesis immediately supplied every modern theorem prover. Resolution and logic programming also required subsequent advances in unification, calculi, and search strategies. Automated reasoning overview

Terms are syntactic objects

Work first in first-order logic without built-in equality, with a nonempty domain. A ground term contains no variables. Given a constant a and a unary function symbol f, ground terms include a, f(a), f(f(a)), and so on. The Herbrand universe is the set of such terms. If the signature has no constant, add a fresh one for this construction.

In a Herbrand interpretation, terms themselves form the domain and functions construct terms. Predicate interpretations select which ground atoms are true. P(a) and P(f(a)) are separate propositional atoms during ground reasoning. This syntactic domain is not a claim that every real-world object literally is a string. Equality needs additional treatment when it is part of the logic. University lecture on Herbrand theory

Worked mechanism: find a finite contradiction

Consider this original clause set, with variables universally quantified:

1. P(a)
2. not P(x) or P(f(x))
3. not P(f(f(a)))

Clause 2 means that if P(x) holds, then P(f(x)) holds. Instantiate it first with x=a, giving not P(a) or P(f(a)). Together with clause 1, this forces P(f(a)). Instantiate again with x=f(a), giving not P(f(a)) or P(f(f(a))). This forces P(f(f(a))), contradicting clause 3.

Only four ground clauses were needed, despite the infinite supply of terms. Rename the atoms A=P(a), B=P(f(a)), and C=P(f(f(a))). The finite problem is A, not A or B, not B or C, not C. Setting A true forces B true and then C true, inconsistent with the final clause. A finite propositional checker can verify this certificate.

This illustrates the unsatisfiability form of Herbrand's theorem for universally quantified clauses after the necessary preprocessing. It does not justify simply deleting arbitrary quantifiers from any formula. Ground-instance theorem

Existential witnesses need dependencies

To use the clause form, existential quantifiers are commonly removed by Skolemization. For forall x exists y R(x,y), replace y by a new function f(x), obtaining forall x R(x,f(x)). The function records that the chosen witness may depend on x. For exists y forall x R(x,y), a fresh constant c suffices because the same witness must work for all x.

These formulas are generally not equivalent as formulas in the same vocabulary. Skolemization preserves satisfiability through expansion or restriction of interpretations in an extended vocabulary. This is exactly the preservation property required for refutation. Dropping witness dependencies changes the problem.

For an original counterexample, use domain {0,1} and let R(x,y) mean x=y. Every x has a y related to it, so forall x exists y R(x,y) holds. No single y equals both 0 and 1, so exists y forall x R(x,y) fails. Replacing every existential witness by one constant would lose valid models. Skolemization and equisatisfiability

Why the procedure may keep searching

Enumerate finite sets of ground instances fairly, testing them for propositional unsatisfiability. If the universal clause set is unsatisfiable, the theorem guarantees a finite witness that the search eventually includes. If it is satisfiable, no contradiction will appear, and a general implementation may keep searching forever. Failure to find a contradiction up to depth 100 is only a bounded search result.

The enumeration must be fair. Always exploring f(f(f(...a))) while ignoring terms built with another function g can miss a short useful instance involving g(a). Completeness of an inference system does not guarantee completeness of every scheduling policy.

Unification lets a prover combine clauses using substitutions without explicitly listing every ground instance first. Resolution removes complementary literals after they have been made compatible. These mechanisms can dramatically change practical search, but there is still no general terminating decision algorithm for unrestricted first-order validity. SAT solvers handle propositional problems; SMT and first-order provers add different theories and mechanisms. They should not all be reduced to one historical invention. Resolution and search

Declarative meaning versus execution order

A logic program can have a clear intended relation while a particular depth-first execution order loops. For example, a recursive clause placed before a terminating fact can repeatedly expand a goal instead of reaching the fact. That does not refute the fact's logical consequence. It exposes the difference between the set of consequences and the operational procedure used to find them.

This distinction also helps assess software tools. Ask what logic they support, what preprocessing preserves, whether their search is fair, and which results carry checkable certificates. A fast run without a proof of the claimed property is not the same as a completed proof.

Exercises

1. Replace clause 3 in the worked example by not P(f(f(f(a)))). List the required instances of clause 2 and the chain of forced atoms.
2. Skolemize forall x exists y forall z exists w S(x,y,z,w). Explain why giving both witnesses one constant changes the meaning. Which property is preserved by correct Skolemization?
3. A prover has found no contradiction after examining all ground terms of depth at most five. Another prover produces four ground clauses and a verified propositional contradiction. What may each report? Explain why the finite certificate is stronger than the longer unsuccessful search.

Compare your reasoning with the worked solutions

1. Use x=a, x=f(a), and x=f(f(a)). Starting from P(a), the instances force P(f(a)), then P(f(f(a))), then P(f(f(f(a)))). The last conflicts with the replacement negative clause. The original fact, three instances, and negative clause form a five-clause certificate. There is no need to enumerate deeper terms after this contradiction is verified.
2. Introduce fresh functions: forall x forall z S(x,f(x),z,g(x,z)). The first witness may depend on x; the second may depend on x and z, with the previously selected y already determined by x. Constants would incorrectly require fixed witnesses for all choices. Correct Skolemization preserves satisfiability in an expanded signature, not ordinary equivalence in the original signature.
3. The first may report no refutation found within its bound, or unknown. It cannot generally declare satisfiable from that alone. The second may report unsatisfiable if the clauses are valid instances of correctly preprocessed input and the contradiction checks. The certificate provides a finite reason that no interpretation satisfies those clauses; search duration and depth are not substitutes for that reason.