A System Cannot Vouch for Itself

Gödel’s second incompleteness theorem says this. A consistent formal system that can express basic arithmetic, and whose axioms can be listed by a program, cannot prove its own consistency. If it could, it would be inconsistent.

The result is often quoted as a vague statement about the limits of the mind. I want to use it for something narrower: what an automated reasoner can and cannot check about itself.

Martin Löb proved a sharper result in 1955. Take any statement P. If the system can prove “if P is provable, then P is true”, then the system can already prove P.

Read it as a trap. Suppose a system adopts the rule “whatever I can prove is true” for every P. By Löb’s theorem it can then prove every P, including falsehoods. So a system cannot trust its own proofs as a general rule. It can trust the proofs of a weaker system. It cannot trust its own at full strength.

Consider a program that rewrites its own code and wants a guarantee that the new version is safe. If the guarantee is a formal proof, something has to check it. If the checker is the new version itself, Löb’s theorem blocks the simplest form of the plan. Each version can fully trust only successors that reason in a strictly weaker system.

Rice’s theorem adds a separate limit. Any non-trivial property of what a program does, as opposed to how it is written, is undecidable in general. No checker can decide, for every program, whether it ever prints a given string.

None of this makes verification useless. It makes it external and partial. You can prove narrow properties of fixed code. You can check outputs against a separate, simpler system. You can use a stronger system to vouch for a weaker one. What you cannot have is a closed loop in which a system certifies its own general reliability.

My view is that this is the real lesson for building reliable agents. Trust has to come from outside the loop: a smaller checker, a test, a person, a world that pushes back. The theorems do not say machines cannot think. They say no reasoner, machine or not, gets to be its own final referee.