Complete and Undecidable

Gödel’s 1929 dissertation established an exact fit between two things that had been kept apart: a sentence true in every model of a theory, and a sentence derivable by the theory’s formal rules.

The result goes by the short name completeness, which invites a conclusion it does not carry. If every truth has a proof, a machine can answer any question by searching for one.

The missing half is what the machine does while the proof fails to arrive.

Church and Turing supplied that half in 1936, within weeks of each other. There is no mechanical procedure that decides validity for an arbitrary first-order formula. First-order logic is complete in Gödel’s sense and undecidable in theirs, and the two statements sit together without any strain at all.

Three words doing three different jobs #

Completeness says a valid sentence has a derivation. A search can enumerate derivations and stop when it finds one.

It does not say an invalid sentence comes with a finite certificate that a blind search must eventually hit. Consistency is a third thing again: a theory is consistent when it does not derive both a formula and its negation. Three terms, three jobs, and none of them is evidence for the others.

Presburger showed the contrast in the same year as Gödel’s dissertation. The natural numbers with addition and equality, but without multiplication, have a theory that is both complete and decidable. Fischer and Rabin later proved that every decision procedure for it has a double-exponential worst-case lower bound.

A procedure can be guaranteed to finish and still be a terrible place to wait.

Adding multiplication changes the status outright. First-order arithmetic with both operations is undecidable, as Tarski and Mostowski showed at mid-century and Robinson extended shortly after. The objects are the same natural numbers throughout.

What moved was the language permitted to describe them.

SAT decides the instance it was handed #

Boolean satisfiability asks whether some assignment makes one propositional formula true. Cook’s 1971 theorem made it the first NP-complete problem, and the answer to a fixed encoded formula settles the encoded hardware, scheduling or model-checking question it came from.

Backtracking search from the early 1960s and the conflict-driven clause-learning framework used by modern solvers turned that into an engineering instrument capable of formulas with tens of thousands of variables and millions of constraints.

This is what a properly bounded rule system looks like. The formula is finite. The vocabulary is fixed. The property being decided is satisfiability, and not an unnamed sense of acceptable behaviour.

A solver may be ruinously expensive and it is still deciding the instance it was given. Open problems in combinatorics have been settled this way, by finite encoding, and not by any solver discovering a universal method.

A Prolog-style policy engine sits differently again. It expresses a live rule base and searches for facts that satisfy it, which is genuinely useful and does not make the general validity problem decidable. Codd’s relational model gives the safer version: a table is a predicate, its rows are the satisfying tuples, and a query evaluates a formula against a finite structure. The finiteness is doing the work in both cases.

Rice drew the hard line #

Rice’s 1951 dissertation gives the general form, and it is more sweeping than people expect.

Every non-trivial semantic property of a program is undecidable. If the property depends on the function a program computes, and is true of some computable functions and false of others, then no algorithm settles it for arbitrary programs. Whether a program always returns zero, or computes a target function, or behaves acceptably, does not become decidable by having passed a large number of examples.

Fred Cohen’s work on computer viruses is the operational case. He had published the theory and experiments in 1984, taking the name at Leonard Adleman’s suggestion; the later result is that no algorithm perfectly detects all possible viruses.

Signature and heuristic scanners are not incomplete because their authors ran out of signatures. They are built on the available side of a boundary a general semantic classifier cannot cross, and everyone building them knows it.

A sound refusal is a result #

Termination analysis is where the discipline becomes visible in ordinary working practice.

Proof assistants reject a recursive definition unless each call can be shown to operate on a structurally smaller argument. Structural decrease is sufficient for termination and is not necessary for it, so every sound general termination analyser leaves infinitely many terminating programs uncertified. The tool declines rather than guesses, and the declining is the feature.

Formal verification succeeds by narrowing the object, never by dissolving the result. Verified kernels and verified compilers each concern one fixed program and one fixed specification, proved once and checked. None of them licenses a general procedure over arbitrary programs and arbitrary properties, and none of them claims to.

The ceiling is not every policy failure #

A compliance rule meeting a new instrument class may have no answer for several quite different reasons. Its terms never classified the instrument. An exception authority has not acted. Successive amendments point in opposite directions.

Those are failures of governance and version control. Calling them undecidability gives the policy more grandeur than it has earned, and it makes the fixable ones look permanent.

The computability result only begins after a formal language, a target property and a class of inputs have been fixed. At that point a reduction can show no general decider exists. Before that point, changing a definition or naming an escalation authority may well settle the case by Thursday.

The two situations look identical from the queue. Both produce an unclosed review, sitting there, with nobody able to say why.

They need different records, and the difference is the whole of what a reviewer needs to know.

A passing suite is the visible proof that the rules answered yesterday’s cases.

A declared fragment, an abstention state and a named escalation path are the quieter proof that they can survive tomorrow’s.