What Happens When a Math Sentence Says “I Am Provable”?
The Warning Label on Every Math System
In 1931, a young Austrian mathematician named Kurt Gödel (1906–1978) published a result that shook the foundations of mathematics. He showed that any formal system strong enough to handle simple arithmetic always contains true statements that cannot be proved inside that system.
To understand this, think of a robot that is programmed to check all true statements about numbers. You would love for the robot to be able to prove that it will never make a mistake — that it will never say “0 = 1.” Gödel’s first incompleteness theorem says the robot cannot do that. If the robot is consistent (it never proves a contradiction), it cannot prove its own consistency.
How did Gödel manage to say something so bold? He invented a way to turn statements about numbers into numbers themselves. Every formula, every proof, gets a unique numerical code called its Gödel number. Then you can write an arithmetical sentence that, when decoded, says something about its own code. The most famous example is a sentence that says, in effect, “I am not provable.” Let’s call it G. If G were provable, the system would prove a false statement (because G says it isn’t provable). So a consistent system cannot prove G. Yet we, standing outside the system, can see that G is true — precisely because it’s unprovable. There is a gap between truth and provability.
The Sentence That Boasts “I Am Provable”
After Gödel, the American logician Leon Henkin (1921–2006) asked a deceptively simple question in 1952. What if, instead of saying “I am not provable,” a sentence said “I am provable”? Suppose a sentence B says, in the coded language, “B is provable in this system.” What can we conclude about B?
Three years later, Leon Löb (1921–2006) gave a shocking answer. It seems natural to think: anything that is provable is true, so if B says it is provable, then B should be true. But Löb proved that a formal system like Peano Arithmetic (the standard theory of basic addition and multiplication) can prove the statement “if B is provable then B is true” only when it already proves B directly. In other words, the system can’t use its own provability as a stepping-stone to reach a new truth. Either the sentence is already a plain theorem, or the system cannot confidently assert that provability implies truth for that sentence.
This result is now called Löb’s theorem. In symbolic form, where □A means “A is provable,” Löb’s theorem says: if the system can prove □(□P → P) → □P is always true, then it must be that if the system proves □P → P, it also proves P. That’s a mouthful, but you can think of it as a limit on self-confidence. A system can’t pull itself up by its own bootstraps.
A Logic Built from Löb’s Surprise
Löb’s discovery didn’t just answer Henkin’s question. It also suggested three simple conditions that any decent provability predicate should satisfy in arithmetic. Together they form the backbone of a new kind of modal logic — provability logic, often called GL (after Gödel and Löb).
In ordinary modal logic, □ can mean “it is necessary that” or “it is known that.” In GL, □ means “it is provable in Peano Arithmetic that.” And the logic runs on one special axiom:
□(□A → A) → □A
That is exactly the principle behind Löb’s theorem, turned into a logical rule. Add it to a basic modal system, and you get GL. This system also proves other surprising things. For example, □⊥ → □¬□⊥ (if a contradiction is provable, then it’s provable that a contradiction isn’t provable) — a direct echo of Gödel’s second incompleteness theorem.
One of GL’s most elegant features is the fixed point theorem. Suppose you have a formula that talks about itself, like “this sentence is not provable.” In GL, you can always find another formula that says exactly the same thing but without any actual self-reference. For instance, the self-referential “I am not provable” turns into the non-self-referential statement that the system cannot prove a contradiction (its own consistency). The theorem says that for any sentence A(p) where the variable p only appears inside □ operators, there is a sentence B with no p that satisfies B ↔ A(B) — and this B is unique up to logical equivalence. So self-reference is never really necessary; you can always rephrase it away.
Worlds Without Loops
How can we check which formulas are actually theorems of GL? One powerful method uses possible worlds semantics. Imagine a collection of toy universes, or “worlds,” connected by arrows that show which world can see which other world. A formula □A is true in a world if A is true in all worlds reachable from it.
For GL, the worlds must be arranged in a particular way: they form a finite, transitive, irreflexive tree. “Transitive” means if world w1 sees w2 and w2 sees w3, then w1 sees w3. “Irreflexive” means no world sees itself. And the tree has no infinite upward paths — you cannot follow arrows forever.
In the early 1970s, logicians like Krister Segerberg proved that GL is sound and complete with respect to these trees. Any formula that is true in every such tree is provable in GL, and vice versa. This gives us a mechanical procedure: to test a formula, you can search through all finite trees of a certain depth. The procedure is efficient enough to belong to the complexity class PSPACE, making GL decidable by a computer with a reasonable amount of memory.
Solovay’s Bridge to Arithmetic
Even with the tree semantics, a big question remained: does GL really capture all reasoning about provability inside arithmetic? In 1976, Robert Solovay (born 1938) proved that the answer is yes, in a spectacular result called arithmetical completeness.
Here’s what that means. Take any modal formula A, like □p ∨ □¬p (which says “either p is provable or its negation is provable”). You can realize it by replacing each propositional variable with an actual sentence of arithmetic and each □ with the formal provability predicate of Peano Arithmetic. Solovay showed that A is a theorem of GL if and only if, for every possible realization, the resulting arithmetical sentence is provable in Peano Arithmetic.
In other words, GL is a perfect miniature version of all the true statements arithmetic can make about its own provability, as long as those statements use only simple propositional structure. If you want to know whether some claim about provability is forced by arithmetic, you can just ask GL — and its answer will always match the real thing.
Solovay’s proof was a masterpiece. He started from the tree completeness of GL: if GL doesn’t prove A, there is a finite irreflexive tree where A is false at the root. Then he constructed a clever arithmetical imitation of that tree, using the diagonalization technique to build sentences that behave like the worlds. The result was a realization that made A false in arithmetic. So arithmetic can’t prove it either. This gave the missing direction: if arithmetic always proves the realizations of a modal formula, then GL must already prove it.
Why It Still Matters When Machines Talk About Themselves
You might think this is all just about numbers and logic puzzles. But the limits discovered by Gödel and Löb echo everywhere. Any computer program that is smart enough to check facts about its own code will hit the same wall. It cannot fully certify itself as bug-free. If a program announces “I can prove that this claim is safe,” that self-trust only works if the claim was already safe from the start.
These results also shape debates about the human mind. Some people say that because machines are limited by Gödel’s theorems but humans can “see” truths outside the system, our minds can never be reduced to a program. Others reply that humans are themselves finite systems and face similar limits, even if we don’t feel them. The mathematics of provability doesn’t settle the argument, but it sharpens the question: when you believe something, can you always explain how you reached that belief — or do you sometimes just jump outside the loop?
In the end, formal provability is one of the most precisely defined concepts in all of mathematics. Unlike words like “truth” or “knowledge,” which can lead to slippery paradoxes, provability inside a fixed system behaves with clockwork regularity. And the logic GL lets us study that clockwork from the inside, showing exactly what a system can and cannot say about itself.
Think about it
- If a robot claims “I can prove this statement,” should you believe it? Under what circumstances would you trust such a claim?
- Suppose you write a sentence on a card: “The statement on the other side of this card is false.” On the other side it says: “The statement on the first side is provable.” What kind of loop does this create?
- Can a person ever fully understand the limits of their own thinking? Why or why not?
