Cantor bewijst met het diagonaalargument dat de reele getallen een niet-aftelbare verzameling vormen.
Turing bewijst met het diagonaalargument dat het stopprobleem voor Turingmachines niet door een Turingmachine opgelost kan worden.
Gödel bewijst met het diagonaalargument dat een consistent formeel systeem dat sterk genoeg is om de rekenkunde te formaliseren uitspraken bevat die waar zijn maar niet binnen dat systeem bewezen kunnen worden.
Voor een sappig betoog over deze en aanverwante zaken, zie Chaitin's The Unknowable. Chaitin zet daar uiteen hoe Berry's paradox (het kleinste natuurlijke getal dat niet in minder dan honderd woorden gedefinieerd kan worden is zojuist met minder dan honderd woorden gedefinieerd) omgezet kan worden in resultaten over de onbeslisbaarheid van vragen naar het kortste programma dat een gegeven resultaat berekent. [Bij een gegeven programma zijn er maar eindig veel kortere, maar die kunnen we niet een voor een uitproberen omdat we niet weten of ze ooit zullen stoppen.]
Laten we een theorie verzinnen en een bewijs opschrijven.
Een groep heeft drie operaties, een tweetallige: (g,h) -> g*h (vermenigvuldigen), een eentallige: g -> g' (inverse nemen), en een nultallige: e (het neutrale element). Er zijn ook axioma's, zeg
Nu het bewijs van de stelling. Het 1-regelige bewijs
Inderdaad, onze taal bestaat uit de symbolen *, ', e, =, (, ), "voor alle", "en", "->" en namen van variabelen: a, b, c, g, h, k. (We weten niet bij voorbaat hoeveel variabelen we nodig hebben, en willen graag dat er altijd genoeg zijn. Een standaardoplossing is er daarom oneindig veel te nemen, zeg a, a1, a11, a111, a1111, ... Dit kost toch maar twee symbolen.) Ken nu een getal toe aan elk symbool in de taal: 1. *, 2. ', 3. e, 4. =, 5. (, 6. ), 7. "voor alle", ..., 15. k. Dan wordt een formule zoals "( voor alle g: (g')' = g)" een rijtje getallen: [5,7,13,5,13,2,6,2,4,13,6]. Maar een rijtje getallen kun je ook weer in een enkel getal coderen, bijvoorbeeld door [a,b] = (2^a)*(3^b) te nemen, en [a,b,c] = [a,[b,c]], enz. Nu zie je dat een rijtje beweringen ook weer in een (heel groot) getal gecodeerd kan worden, zodat uiteindelijk het hele bewijs een heel groot getal geworden is. (Een heel andere manier is het bewijs gewoon uitschrijven in ASCII, dan alle bytes achter elkaar zetten, en lezen als een groot binair getal.)
OK. Dus een bewijs kan als een getal gecodeerd worden, en we kunnen mechanisch controleren of een bewijs correct is. De controleur moet uit [a,b] weer a en b terug kunnen vinden, dus een beetje kunnen rekenen.
Stel je nu voor dat ons onderwerp niet de groepentheorie was, maar de rekenkunde, met constante symbolen +,-,*,/,0,1 en logische symbolen "en", "of", "niet", "voor alle", "er is een", en axiomas voor de elementaire rekenkunde. Dan kunnen we een formule opschrijven die zegt
"het getal M codeert een bewijs van de bewering met code B"
en ook een formule F(x,y) die zegt
"er is geen getal M dat de code is van een bewijs van de bewering die ontstaat als we in de formule met code x voor alle vrije variabelen het getal y invullen".
Laat die laatste formule code f hebben. Dan zegt F(f,f):
"ik kan in deze theorie niet bewezen worden".
Zou dat waar zijn? Wel, als F(f,f) een bewijs heeft in de gegeven theorie, dan is er dus een groot getal M dat een bewijs is van de bewering F(f,f), maar als een getal een bewijs is van een bewering dan is die bewering ook waar, en geldt F(f,f) die zegt dat er niet zo'n M is. Tegenspraak. OK. Dus F(f,f) heeft geen bewijs in de gegeven theorie. Maar dat betekent dat F(f,f), die zegt dat hij niet bewezen kan worden, de waarheid spreekt. Het is een ware uitspraak die niet bewezen kan worden binnen de theorie (maar die we zojuist bewezen hebben).
Dit diagonaalargument levert dus:
Gegeven een theorie die een fragment van de rekenkunde bevat dat groot genoeg is om uit [a,b] weer a en b terug te vinden, en die ook de eerste orde predicatenlogica (met "en", "of", "niet", "voor alle", "er is een") bevat, dan ňf je kunt alles bewijzen in die theorie (hij is niet consistent), ňf er zijn ware beweringen in die theorie die je niet binnen de theorie bewijzen kunt. Dit is Gödels onvolledigheidsstelling.
Een voorbeeld van een theorie waarin alle ware uitspraken ook bewezen kunnen worden is de meetkunde van het platte vlak. Kennelijk is die theorie niet groot genoeg om er de rekenkunde in te kunnen formuleren.