Gödel II. nemteljességi tétele

1. Fixpont tétel: Legyen Γ olyan, hogy abban minden rekurzív függvény reprezentálható. Ekkor minden χ(x) egyváltozós formulához van olyan Ψ (szabad váltózó nélküli formula) fixpont, amivel

Γ |− Ψ ↔ χ(⌈Ψ⌉).

(Lásd a logika jegyzetben.)

2. Legyen Γ olyan, hogy abban minden rekurzív függény reprezentálható. Legyen még Δ egy rekurzív elmélet; Az, hogy “u egy Δ-beli levezetése i-nek” egy rekurzív reláció, legyen ennek egy Γ-beli reprezentánsa Prov_{Δ}(u, i), továbbá legyen Pr_{Δ} az alábbi módon definiált egyváltozós formulája Γ-nak:

(1)  Pr_{Δ}(i) =^{def} ∃u Prov_{Δ}(u, i).

Az, hogy a Δ konzisztens azt jelenti, hogy nem vezethető le belőle a hamis, legyen tehát

(2)  Con_{Δ} =^{def} ¬Pr_{Δ}(⌈hamis⌉).

Itt “hamis” az azonosan hamis formulát jelöli, ennek a Gödel számát kell vennünk a Γ-beli reprezentációnál választott kódolásnál.

Tétel (Rosser) Tegyük fel, hogy Γ rekurzív és Γ-ban minden rekurzív függvény reprezentálható. Ekkor van a Γ-ból való levezethetőségnek olyan Prov_{Γ}^{∗} reprezentáló formulája, hogy az ebből (1) és (2) alapján definiált Con_{Δ}^{∗} formulára

Γ |− Con_{Δ}^{∗}.

Bizonyítás Ha Γ ellentmondásos, akkor ez persze így van, és semmit nem kell bizonyítanunk. Feltehetjük tehát, hogy Γ ellentmondástalan, vagyis belőle nem vezethető le egyszerre egy formula és a tagadása is. Legyen n(x) az x kódú formula lezártjának majd negáltjának a Gödel-száma, mivel ez rekurzív függvény azért reprezentálható, úgy képzeljük hogy az n relációjel éppen őt reprezentálja (ezt az adódó formula egyszerűbb felírhatósága miatt tesszük, egyébként nyugodtan be lehetne írni a megfelelő definíciót a formulába). Legyen Prov_{Γ} a levezethetőség egy reprezentáló formlája, és legyen

Ψ(u, i) =^{def} Prov_{Γ}(u, i) ∧ ∀v(v ≤ u → ¬Prov_{Γ}(v, n(i)))

Állítjuk, hogy Ψ és Prov_{Γ} ugyanazt a relációt reprezentálája, ami világos abból, hogy Γból nem lehet egyszerre levezetni egy formulát és a tagadását. Ez lesz a megfelelő Prov_{Γ}^{∗}. Ugyanis n(⌈hamis⌉) = ⌈igaz⌉ és Γ |− igaz miatt van ennek a levezetésnek Gödel-száma, vagyis olyan N sztenderd természetes szám, hogy az N-nek megfelelő k(N) kifejezéssel

Γ |− Ψ(k(N), ⌈igaz⌉),

és persze ugyanerre az N-re

Γ |− Prov_{Γ}(k(N), ⌈igaz⌉)

is fennáll. Ha most Γ egy tetszőleges 𝔄 modelljében volna olyan u elem, amire a tétel állításával ellentétben 𝔄 ⊧ Ψ(u, ⌈hamis⌉) akkor Ψ definíciója szerint

𝔄 ⊧ Prov_{Γ}(u, ⌈hamis⌉) ∧ ∀v(v ≤ u → ¬Prov_{Γ}(v, ⌈igaz⌉)

és így erre az u-ra speciálisan 𝔄 ⊧ ¬(k(N) ≤ u) is fennáll. Viszont a reprezentálhatóság miatt ez csak akkor fordulhat elő, ha u egy N-nél kisebb N′ természetes számhoz rendelt kifejezés értéke, vagyis valamilyen N′ < N természetes számra

𝔄 ⊧ Prov_{Γ}(k(N′), ⌈hamis⌉).

A Prov_{Γ} a levezethetőség egy Γ-beli reprezentációja volt, ezért az N′ szükségképpen egy valódi levezethetés kódja, és így Γ-ból levezethető a hamis, ellentétben feltételezésünkkel. QED

Gödel II nem-teljességi tétele az mondja ki, hogy a levezethetőséget reprezentáló formulára tett bizonyos “természetességi” feltételezések mellett ennek éppen az ellenkezője igaz, vagyis Γ-ból Con_{Γ} nem vezethető le. A Γ indexet az alábbiakban lehagyjuk a könnyebb olvashatóság kedvéért.

Tétel (Gödel II nem-teljességi tétele) Tegyük fel hogy a Γ formulahalmazban a Pr(x) formula a levezethetőség definíciójából állott elő mint fent, és teljesíti a következő feltételeket: F1 Minden φ zárt formulára Γ |− φ esetén Γ |− Pr(⌈φ⌉). F2 Γ |− Pr(⌈φ⌉) → Pr(⌈Pr(⌈φ⌉)⌉). F3 Γ |− Pr(⌈φ⌉) ∧ Pr(⌈φ → ψ⌉) → Pr(⌈ψ⌉). Ilyen feltételek mellett Γ |−̸ Con_{Γ}.

A bizonyítás előtt néhány megjegyzés. Az F1 csak annak megismétlése, hogy Pr_{Γ} jól reprezentálja a levezethetőséget, ennek külön kikötésére nem volna szükség. Az F2 helyett általában csak annyit tudunk, hogy ha Γ |− Pr(⌈φ⌉), akkor Γ |− Pr(⌈Pr(⌈φ⌉)⌉), vagyis ha Γ összes modelljén igaz a Pr(⌈φ⌉) formula, akkor ugyancsak az összes modellen is igaz lesz a másik is. F2 viszont azt köti ki, hogy amennyiben Γ-nak egy tetszőleges modelljében a Pr(⌈φ⌉) igaz, akkor ugyanebben a modellben a hosszabb formula is igaz legyen függetlenül Γ többi modelljeitől. Meg lehet mutatni (bonyolult formulaindukcióval), hogy amennyiben Γ-nak a Peano-t, ZFC-t, vagy egy ezek valamelyikét tartalmazó rekurzív axiómarendszert választjuk, a levezethetőség reprezentációjaként pedig egy megfelelő formulát (a reprezentációs tétel sztenderd bizonyítása egyébként – kisebb átalakításokkal – ilyen formulát ad), akkor F1–F3 teljesül.

Lemma (Gödel) Legyen ν az a (fixpont tétel szerint létező) formula, amire Γ |− ν ↔ ¬Pr_{Γ}(⌈ν⌉). Ha Γ ellentmondástalan, akkor Γ |−̸ ν.

Bizonyítás Tegyük fel, hogy Γ |− ν, megmutatjuk, hogy Γ ellentmondásos. Van tehát ν-nek levezetése Γ-ból, tehát valamilyen N természetes számra Γ |− Prov_{Γ}(k(N), ⌈ν⌉), ahonnan Γ |− ∃uProv_{Γ}(u, ⌈ν⌉). A Pr_{Γ} és ν definíciója miatt ez az jelenti, hogy Γ |− ¬ν. A feltevésünkkel összevetve kapjuk, hogy Γ ellentmondásos. QED

A fenti F1–F3 feltételek még egy nagyon hasznos következményét is igazoljuk:

F4 Ha Γ |− φ → ψ akkor Γ |− Pr(⌈φ⌉) → Pr(⌈ψ⌉).

Ilyenkor ugyanis F1 szerint Γ |− Pr(⌈φ → ψ⌉). Ha most ezt és F3-at egy modus ponenssel összekötjük, éppen a bizonyítandó állítást kapjuk.

Gödel-tétel Bizonyítása Az előző lemma miatt elegendő belátnunk, hogy a Γ-ra tett feltevések mellett Γ |− ν ↔ Con_{Γ}.

Γ |− hamis → ν  tautológia
Γ |− Pr(⌈hamis⌉) → Pr(⌈ν⌉)  F4
Γ |− ¬Con_{Γ} → ¬ν  előző átírása más jelöléssel

Ez adja az ekvivalencia felét. A másikhoz legyen a rövidség kevéért φ =^{def} Pr(⌈ν⌉).

Γ |− Pr(⌈ν⌉) → Pr(⌈φ⌉)  F2 másképp
Γ |− ν → ¬φ  ν definíciója átírva
Γ |− Pr(⌈ν⌉) → Pr(⌈¬φ⌉)  F4
Γ |− φ → (¬φ → hamis)  tautológia
Γ |− Pr(⌈φ⌉) → (Pr(⌈¬φ⌉) → Pr(⌈hamis⌉)) F4 kétszeri alkalmazásával
Γ |− Pr(⌈ν⌉) → Pr(⌈hamis⌉)  az első és harmadik sorból az előző segítségével, egyszerű átalakítással.

Ezzel megkaptuk az ekvivalencia másik felét. QED

Tétel (Löb) Teljesítse Γ a fenti feltételeket, és tegyük fel, hogy valamilyen φ zárt formulára Γ |− Pr(⌈φ⌉) → φ. Ekkor Γ |− φ.

Az állítást az azonosan hamis formulára alkalmazva speciális esetként kiadódik az előző tétel.

Bioznyítás A fixpont tétel szerint van olyan μ zárt formula, amire Γ |− μ ↔ (Pr(⌈μ⌉) → φ). Most

Γ |− μ → (Pr(⌈μ⌉) → φ)  μ definíciója
Γ |− Pr(⌈μ⌉) → (Pr(⌈Pr(⌈μ⌉)⌉) → Pr(⌈φ⌉)) F4 kétszeri alkalmazásával
Γ |− Pr(⌈μ⌉) → Pr(⌈Pr(⌈μ⌉)⌉)  F2
Γ |− Pr(⌈μ⌉) → Pr(⌈φ⌉)  előző kettő, logika
Γ |− Pr(⌈φ⌉) → φ  feltétel
Γ |− Pr(⌈μ⌉) → φ  előző kettő, logika
Γ |− μ  mert a μ éppen ez
Γ |− Pr(⌈μ⌉)  F1
Γ |− φ  hiszen előző → φ már volt

QED