The instance that has to be guessed

The rung below proved that its method terminates, and the argument was one line: every rule replaces a formula by strictly shorter ones, a quantity of whole numbers that strictly decreases cannot decrease forever, so every branch finishes and the tree is finite.

Add quantifiers and that argument fails at one rule, and everything follows from the failure.

The rule that keeps its own formula #

A universal claim $\forall x\,A(x)$ on a branch says $A(t)$ for every term $t$ there is. The rule for it adds one instance, and it cannot discard the universal, because a term that has not appeared yet may appear later and the claim will be needed again.

So a branch grows without any formula being shortened. The undecomposed material on it does not decrease; it does not even stay the same, since each step adds an instance and keeps the source. The termination argument has nothing to work with.

The existential quantifier, by contrast, is harmless. $\exists x\,A(x)$ on a branch is replaced by $A(c)$ for a fresh constant $c$ — one appearing nowhere else — and the existential is then discarded, because one witness is all the claim asserts. That rule shortens the branch exactly as a propositional rule does.

So the two quantifiers behave completely differently and only one of them is the problem. The asymmetry is the same one that runs through the whole of logic: an existential claim is satisfied by one thing and a universal claim is a promise about every thing, so evidence for the first is finite and evidence for the second is not. The rule that cannot discard its own formula is the rule for the quantifier whose content is infinite, and the correspondence is exact rather than suggestive.

That is not a defect of the tableau method. The same failure appears in every proof system for first-order logic and it is not a failure of any of them — it is a fact about the logic, and no procedure of any kind can decide first-order validity, which Church and Turing proved independently in 1936.

What survives is a semi-decision procedure. A search for a proof will find one if there is one, since the correct instances eventually get tried. If there is none, it may run forever, and no amount of running tells the difference between “no proof yet” and “no proof”.

Watching it run #

The figures do the search in the tidiest available form. Instead of building the tree, they instantiate the universal at each term of a growing supply — $a$, then $f(a)$, then $f(f(a))$ — and ask at each stage whether the resulting propositional formula is already contradictory.

That question is decidable, and the figures answer it by brute force over the atoms, which is the same complete procedure the rung below cross-checks against. So each row of the table is a question that is settled; what is not settled is the row after it.

For the first question the answer arrives. The chain $P(a)$, $P(a) \to P(f(a))$, $P(f(a)) \to P(f(f(a)))$, $P(f(f(a))) \to P(f(f(f(a))))$ forces $P(f(f(f(a))))$, so three instantiations are enough and two are not — and the figure checks both halves of that, requiring the earlier stages to have a model and every later one to have none.

The second figure is the situation the whole rung is about. Every row says not yet, and the rows are what a search produces; a reader can see that the answer is no, and the reader is doing something the search cannot, which is reasoning about the whole sequence rather than about its terms.

Why the expansion is the whole story #

That reduction — from a quantified question to a growing sequence of propositional ones — is not a simplification for the sake of a figure. It is a theorem.

Herbrand’s theorem says a first-order formula in the right normal form is unsatisfiable exactly when some finite set of its ground instances is unsatisfiable, where the ground terms come from the formula’s own function symbols and constants. So a first-order refutation is always, at bottom, a propositional refutation of finitely many instances.

That is a striking reduction and it does not make anything decidable. The theorem says a finite set suffices if one does; it gives no bound on how large, and no way to know when to stop looking. The search space is a sequence of decidable questions with no computable stopping rule, which is exactly what semi-decidable means.

It also explains where the difficulty is concentrated. Choosing the right instances is the whole problem, and a modern prover’s cleverness is entirely in that choice — unification, which computes the most general instance that could possibly close a branch rather than trying terms in order.

Why the two cases cannot be told apart #

The uncomfortable half of the situation is not that a search may run forever. It is that a search running is indistinguishable from a search that will run forever, and it is worth being precise about why no cleverness fixes it.

Suppose there were a procedure that, given a formula, reported “no proof exists” whenever that is so. Combined with the search — which reports “proof found” whenever that is so — it would decide validity, by running both and waiting for whichever answers. Church and Turing’s theorem says no such decision procedure exists, so no such reporter exists either.

So the asymmetry is forced rather than a gap in the technique. It is not that nobody has found the stopping rule; it is that a stopping rule would combine with what already exists to produce something that provably does not.

The same argument settles a related hope. A bound on how many instantiations a valid formula needs, as a function of its size, would also give a decision procedure — run the search that far and report failure. So no computable bound exists, and the number of instances a proof needs is not bounded by anything computable in the formula’s length.

That is a considerably stronger statement than “sometimes it takes a while”. There are valid formulas of modest size whose shortest proof requires a number of instantiations larger than any function a person would write down.

What is still true #

The loss is exactly one property, and it is worth listing what survives, because the list is longer than the loss suggests.

Completeness survives. Gödel’s completeness theorem, from 1929, says every valid first-order formula has a proof. The search will find it. What is lost is knowing in advance how long that takes.

Soundness survives. Anything the search proves is valid, which is the direction that matters for trusting an answer when one arrives.

Compactness survives, and it is the reason Herbrand’s theorem holds: if every finite subset of an infinite set of formulas is satisfiable, the whole set is. So an infinite branch that never closes really does describe a model, and the failure to terminate is not a failure to be right.

That last point deserves to be stated as the consolation it is. A propositional tableau that stays open hands over a counterexample in a line — the branch’s literals are an assignment. A first-order tableau that stays open forever hands over a counterexample too, and it is a countable model built one formula at a time; the branch is the model, described by an infinite list of facts about it. The non-terminating run is not producing nothing; it is producing the answer, in instalments, with no last instalment.

What makes that unsatisfying is entirely the finiteness of anybody reading it. The mathematics is behaving correctly and completely: there is no proof, there is a model, and the procedure is exhibiting the model. It simply never finishes exhibiting it, and a reader wanting a verdict rather than a description has asked for something the situation does not contain.

And the subformula property survives — the property the rung below is about — in a modified form. The formulas appearing are instances of subformulas rather than subformulas, which is a much larger set — infinite rather than finite — and that enlargement is precisely the termination argument’s loss, restated.

The three levels, in order #

Putting the ladder’s four rungs against each other gives a sequence worth holding, because each level loses one thing.

Propositional logic is decidable. A truth table always answers, a tableau always terminates, and the only question is cost.

First-order logic is semi-decidable. A proof will be found if there is one; the absence of a proof is not detectable. The property lost is termination on negative instances.

Arithmetic is neither. There are true statements with no proof at all, so even an infinitely patient search fails — the sentence that says it has no proof is the standing example. The property lost is completeness itself.

Each step costs one property and buys expressiveness, and the sequence is not a series of technical accidents. It is the same trade at three scales: a language able to say more about itself is a language whose truths outrun its proofs.

Where the account needs care #

Herbrand’s theorem needs a normal form. The formula has to be Skolemised — existential quantifiers replaced by function symbols — before the expansion is the right object. Skolemising preserves satisfiability and not validity, which is why refutation is the setting rather than direct proof.

The Herbrand universe can be infinite in a way that matters. With one constant and one one-place function it is $a$, $f(a)$, $f(f(a))$ and so on — countable and easy to enumerate. With two functions of two arguments it is a tree of terms growing exponentially, and enumeration in order is hopeless long before the right instance appears.

The figures’ second case is satisfiable, not merely unproved. $P(b)$ genuinely does not follow, so the search is looking for something that is not there. That is the typical non-terminating case; there is no way to tell it from a case where the proof exists and is very deep.

And the propositional check has its own cost. Each stage is settled by trying every assignment, which doubles with each new atom. The figures stop at a handful of stages for that reason, and a real prover does not enumerate assignments either.

What a prover does instead of enumerating #

Nothing practical instantiates terms in order, and the reason is arithmetic rather than taste.

With one constant and one one-place function the Herbrand universe is a list and enumeration is feasible. With two constants and one two-place function it is a binary tree of terms, and the number of terms of depth $d$ grows doubly exponentially; the instance that closes a branch is typically at some depth nobody would reach.

Unification is the repair and it inverts the question. Instead of choosing a term and seeing whether the branch closes, it asks: what is the most general substitution that would close it? Two literals close a branch when one is the negation of the other, so the question is which substitution makes two terms identical, and there is an algorithm computing the most general such substitution or reporting that none exists.

The gain is that the search is now driven by the formulas rather than by the term supply. A branch closes when unification says two of its literals can be made to clash, and the substitution it returns is the instance — found rather than guessed.

What unification does not do is restore termination. The search is still unbounded: a branch may need a universal instantiated many times with different substitutions, and nothing bounds how many. What changes is that the instances tried are the ones that could possibly help, which is the difference between a search that finishes on real problems and one that does not finish on any.

That is the standing situation for every hard search problem in this collection. A dissection’s piece count has no lower-bound method and constructions are found by ingenuity; an equilibrium’s location is guaranteed by a potential and reached by a process nobody has bounded. A guarantee of existence and a method that finds it quickly are separate achievements, and the second is where all the engineering is.

Where the boundary was drawn #

Hilbert posed the Entscheidungsproblem in 1928: find a procedure deciding whether a first-order formula is valid. Church and Turing answered it independently in 1936, and negatively, by different routes — Church through the lambda calculus, Turing through machines — and the two proofs are the founding documents of computability.

The sequence of results either side of that is worth having in order. Gödel proved completeness in 1929: every valid formula is provable. Gödel proved incompleteness in 1931: arithmetic has true statements that are not. Church and Turing proved undecidability in 1936: there is no procedure deciding validity. Herbrand’s theorem is 1930, and it is the positive result the other three are the boundary of.

Completeness and undecidability are not in tension, and the pair is the whole content of this rung. Every valid formula has a proof, and no procedure finds it in bounded time or reports its absence. A search that always succeeds eventually and never announces failure is exactly what those two theorems together describe.

What the pictures cannot show #

The tables show five stages and the sequence is infinite. For the first question that is enough, since the answer arrives at stage three and every later stage agrees. For the second it is not enough and cannot be: the claim is that no stage ever closes, and no finite table establishes it.

That is the honest limitation and it is unusually consequential. The figure showing a search that does not terminate is a figure showing five rows of a search, and a reader concluding “it never terminates” is reasoning about the premises rather than reading the table. The table’s own content is “not yet, five times”.

Nor does anything here draw the tree the search actually builds. The expansion is the tidy form of the search and a real tableau for these formulas would branch, reuse the universal at chosen terms, and be considerably larger — and the figures use the expansion because it is the form where each stage is a question with an answer.

The ladder from here #

Rungs above: unification, which chooses instances by computing the most general term that could close a branch rather than by enumerating. Skolemisation and the normal forms Herbrand’s theorem needs. The decidable fragments — monadic first-order logic, the two-variable fragment, the guarded fragment — which are the parts of the language where termination survives, and which is where description logics come from. Model checking, which is decidable because it fixes a finite model rather than quantifying over all of them. And the arithmetical hierarchy, which classifies exactly how undecidable a question is.

One rule that does not shrink anything #

The habit is about where to look when a procedure stops terminating.

The propositional argument was a measure: a quantity that decreases at every step and cannot decrease forever. That is the standard way to prove anything terminates, and this collection has now used it on a tableau, on a congestion game’s potential and on Euclid’s algorithm.

When a procedure fails to terminate, the question is therefore not “why does it run forever” but “which step fails to decrease the measure” — and here the answer is a single rule, identifiable, with a reason attached: the universal is kept because a later term may need it.

That precision is what makes the failure informative rather than merely disappointing. Knowing which rule breaks the argument says immediately where to look for decidable fragments: restrict the language so that the supply of terms is finite, and the rule can only fire finitely often, and termination comes back. Every decidable fragment of first-order logic is that observation applied in a different way.