Először is, “bizonyítottnak lenni” számomra azt jelenti, hogy “bizonyítottnak lenni a matematika egésze által”. Mint jól tudjuk, kettő meg kettő az négy. És természetesen bizonyítható, hogy kettő meg kettő az négy (vagyis bizonyítható a matematika egésze által, habár a kettő meg kettő esetében persze nincs szükség a matematika egészére annak bizonyításához, hogy az négy). Talán ez már nem annyira világos, de az is bizonyítható, hogy bizonyítható, hogy kettő meg kettő az négy. És az is bizonyítható, hogy bizonyítható, hogy bizonyítható, hogy kettő meg kettő az négy. És így tovább. A helyzet az, hogy ha egy állítás bizonyítható, akkor az is bizonyítható, hogy az állítás bizonyítható. És még ez is bizonyítható.

Kettő meg kettő az nem öt. És bizonyítható, hogy kettő meg kettő az nem öt. És bizonyítható, hogy bizonyítható, hogy kettő meg kettő az nem öt, és így tovább.

Így tehát: bizonyítható, hogy kettő meg kettő az nem öt. Vajon bizonyítható az is, hogy kettő meg kettő az öt? Hogy finomak legyünk, nagy csapás lenne a matematikára nézve, ha ez bizonyítható volna. Ha bizonyítható volna, hogy kettő meg kettő az öt, akkor az is bizonyítható volna, hogy az öt az nem öt, és akkor nem létezne egyetlen olyan állítás sem, amelyik ne volna bizonyítható, vagyis a matematika egy rakás sületlenség volna.

Ezért akarjuk megkérdezni: bizonyítható-e, hogy nem bizonyítható, hogy kettő meg kettő az öt? Merő döbbenet: nem bizonyítható! Pontosabban: ha bizonyítható, hogy nem bizonyítható, hogy kettő meg kettő az öt, akkor az is bizonyítható, hogy kettő meg kettő az öt, és ekkor a matematika nem más, mint egy rakás sületlenség. Valójában ha a matematika nem egy rakás sületlenség, akkor nem bizonyítható egyetlen olyan formájú állítás sem, hogy “az X állítás nem bizonyítható”.

Vagyis amennyiben a matematika nem egy rakás sületlenség, úgy, bár az nem bizonyítható, hogy kettő meg kettő az öt, de az sem bizonyítható, hogy nem bizonyítható, hogy kettő meg kettő az öt.

Mellesleg ha már itt tartunk, akkor elárulom: igen, bizonyítható, hogy ha bizonyítható, hogy nem bizonyítható, hogy kettő meg kettő az öt, akkor bizonyítható, hogy kettő meg kettő az öt.

“Bárcsak megmagyarázná ezt a magyarázatot!”

Ha a matematika egésze formalizálható egy szokásos felépítésű formális elméletben, mint ahogy azt fel fogjuk tenni (bár ez nem kis feltevés), akkor létezik a (z elmélethez tartozó) nyelvben egy olyan, az elmélet (“mint” formális elmélet) megfelelő leírásából nyerhető formula: Proof(x, y), amelyik teljesíti e három feltételt:

(i)      ha |¾p, akkor |¾ □p ,
(ii)     |¾ (□(p®q) ® (□p® □q)) , és
(iii)    |¾ (□p® □□p)

Az (i), (ii) és (iii) feltételeket Hilbert-Bernays-Löb-féle levezethetőségi feltételeknek nevezik; minden olyan ésszerű formális elmélet teljesíti őket, amelyikben az aritmetika egy bizonyos kis része bizonyítható.

Minthogy az elmélet standard, benne a nyelvének minden tautológiája bizonyítható, valamint a bizonyítható kijelentések minden logikai következménye is bizonyítható.

Ebből következik, hogy minden p, q mondatra

(iv)    ha |¾ (p®q), akkor |¾ (□p ® □q).

^ az a nullaargumentumú igazságfüggvény, amelyik minden kiértékelés mellett hamis. Természetesen ^ egy ellentmondás. Később majd észre kell vennünk, hogy (Øq® (q ® ^)) egy tautológia. Ha ^ nem tartozik a nyelv primitív szimbólumai közé, akkor bármely elvetendő mondattal definiálhatjuk, például azzal, amelyik kifejezi, hogy kettő meg kettő az öt.

^ segítségével könnyen kifejezhetjük az elmélet konzisztenciáját:Ø|¾ ^ , azaz ^ nem bizonyítható az elméletben. A nyelv azon mondata, amelyik az elmélet konzisztenciáját állítja, Ø□ ^alakúnak vehető, mely azonos azzal, hogy Ø$xProof(x, é^ù ).

Immár bebizonyíthatjuk Gödel második nemteljességi tételét, amely azt állítja, hogy amennyiben az elmélet konzisztens, úgy a nyelv azon mondata, amelyik az elmélet konzisztenciáját állítja, nem bizonyítható az elméletben – csakúgy, mint azt a tételt, mely szerint a második nemteljességi tétel bizonyítható az elméletben (“formalizált második nemteljességi tétel”).

A diagonalizálási eljárás segítségével, melyet Gödel vezetett be “A formálisan eldönthetetlen kijelentésekről…” című írásában, található egy olyan p mondat, amelyik ekvivalens az elméletben azzal a kijelentéssel, hogy p bizonyíthatatlan az elméletben, vagyis egy olyan mondat, hogy

1. |¾ p « Ø□p
2. |¾ p ® Ø□p                                                  1-ből igazságfüggvény szerint
3. |¾ □p ® □Ø□p                                            2-ből (iv) alapján
4. |¾ □p ® □□p                                               (iii) alapján
5. |¾ Ø□p ® (□p ® ^)                                     tautológia
6. |¾ □Ø□p ® □(□p ® ^)                                 5-ből (iv) alapján
7. |¾ □(□p ®^) ® (□□p® □^)                        (ii) alapján
8. |¾ □p ® □^                                                 3, 6, 7, és 4-ből igazságfüggvény szerint
9. |¾ Ø□^® p                                                   8 és 1-ből igazságfüggvény szerint
10. |¾ □Ø□^ ® □p                                              9-ből (iv) alapján
11. |¾ Ø□^ ® Ø□Ø□^                                      8 és 10-ből igazságfüggvény szerint.

Így ha |¾ Ø□^ , akkor mind |¾ Ø□Ø□^ , mind (11), és (i) alapján |¾ □Ø□^ , ahonnan, a propozicionális kalkulus alapján, |¾^. Tehát ha Ø|¾ ^ , akkor Ø|¾ Ø □ ^ .