How a proof system can talk about its own proofs
Gödel’s key move was to turn statements and proofs into objects arithmetic could describe. By assigning numbers to symbols and sequences of symbols—a method now called Gödel numbering—a formal system can express facts about whether a particular sequence counts as a valid proof.
That makes it possible to construct a sentence that, in effect, says: “There is no proof of this sentence in this system.” The wording is not a loose paradox; the system’s rules encode the claim as a precise statement about numbers and proofs.
The gap between truth and proof
If the system is consistent—that is, its rules do not let it prove contradictions—it cannot prove the sentence. If it did, it would prove a statement asserting that it has no proof. Under the usual interpretation of arithmetic, the sentence is therefore true, even though the system cannot establish it from its own rules.
This result applies to formal systems that can be mechanically specified and contain enough arithmetic to carry out the encoding. It does not mean every mathematical claim is unknowable, or that ordinary calculations are suspect. It means no such system can capture every arithmetic truth using only its own proof rules.
Why adding a rule does not end the problem
Mathematicians can add the unprovable sentence as a new axiom, expanding the system. But the expanded system is still a rule-governed system of the same general kind, so Gödel’s argument produces a new statement it cannot prove. The blind spot moves rather than vanishes.
A related result sharpens the limitation: under the same broad conditions, a consistent system cannot prove its own consistency from within. To certify its reliability, it must lean on assumptions or reasoning beyond the system itself.
