Szerkesztő:Thuluviel/Idézetek/provlog

A bizonyíthatósági logika a modális logika azon fejezete, amelyben egy modális kijelentés olyan módon igaz, hogy bizonyítható egy formális rendszerben, pl. egy (intuicionista) logikában, Peano-aritmetikában, halmazelméletben. A bizonyíthatósági logika célja tehát egy adott formális rendszerben a bizonyíthatóság-fogalom megragadása. A bizonyíthatóságot e nyelvben egy $\scriptstyle {\Box }$ jellel szokás jelölni.

Példák

Intuicionista logika

Az intuicionista logikánál az egyik alkalmas fordítás úgy néz ki, hogy minden atomi mondat és negációjel elé egy $\scriptstyle {\Box }$-ot kell írni, így pl. egy, a kizárt harmadik elvét képviselő formula a következő alakot ölti:

$\scriptstyle {p\vee \lnot p\quad \rightsquigarrow \quad \Box p\vee \Box \lnot \Box p}$

Szóban mondva a „$\scriptstyle p$ állításnak rendelkezünk a bizonyításával, vagy a bizonyíthatóságának cáfolatával”. A modális logikából ismert lehetséges világok itt episztemikus helyzeteket képviselnek; a világban szereplő $\scriptstyle \Box A$ alakú formulák azok a formulák, melyeknek van bizonyításuk, azaz itt és már minden rákövetkező tudásállapotban rendelkezésünkre kell álljon az $\scriptstyle A$.

A fenti formula azonban a következő ábra (modális logikai modell) miatt hamis is lehet, így a kizárt harmadik törvényét képviselő formula nem logikai igazság - ami az intuicionista logikából valóban levezethetetlen. Ugyanis ha az alsó 'tudásállapotban' helyezkedik el a $\scriptstyle \Box p\vee \Box \lnot \Box p$ formula, akkor ez valóban hamis lesz, mivel egyrészt $\scriptstyle \Box p$ valóban nem igaz, hiszen a baloldali világban nem igaz, másrészt pedig $\scriptstyle \Box \lnot \Box p$ sem igaz, mivel a jobboldali világnak minden rákövetkezőjében (azaz önmagában) igaz a $\scriptstyle p$.

Ez a fordítás a nulladrendű intuicionista logikát az S4 modális logikába fordította. Modális logikai szemszögből tehát azt mondhatjuk, hogy az S4 kalkulusnak két (adekvát) szemantikája lehetséges, az egyik a Kripke-szemantika, a másik pedig a nulladrendű intuicionista logika.

Peano-aritmetika

A Peano-aritmetika egy fordítása úgy néz ki, hogy a Peano-aritmetikában szereplő azon $\scriptstyle {Lev}$ predikátumot, mely a levezethetőséget kódolja, írjuk át $\scriptstyle \Box$-ra. Mivel $\scriptstyle {Lev}$ a Peano-aritmetikában lévő levezethetőségnek felel meg, így $\scriptstyle \Box$ rajta keresztül itt is a bizonyíthatóságot ragadja majd meg.

A Peano-aritmetikára illeszkedő (Gödel és Löb után) GL modális logikában ha nézzük mondjuk a következő formulát:

$\scriptstyle {\Box \lnot \Box \bot \quad \rightsquigarrow \quad Lev(\ulcorner \lnot Lev(\ulcorner 0=1\urcorner )\urcorner )}$

Ez a formula, ha a fordítás tényleg jó, nem lehet tétel. Azt fejezi ugyanis ki, hogy „levezethető, hogy nem bizonyítható az ellentmondás”, azaz hogy bizonyítható az aritmetika konzisztenciája -- ennek azonban maga Gödel második nemteljességi tétele állja útját.

A GL-ről tehát majd azt mondhatjuk, hogy két szemantika adható rá; az egyik a szokásos Kripke-szemantika, a másik pedig maga a Peano-aritmetika.

Bizonyíthatósági logikák

Intuicionista logika

S4

IPC lefordítása S4-re
$\scriptstyle {[p]}$	$\scriptstyle {\Box p}$
$\scriptstyle {[\lnot A]}$	$\scriptstyle {\Box \lnot [A]}$
$\scriptstyle {[A\rightarrow B]}$	$\scriptstyle {[A]\rightarrow [B]}$
$\scriptstyle {[A\vee B]}$	$\scriptstyle {[A]\vee [B]}$
$\scriptstyle {[A\land B]}$	$\scriptstyle {[A]\land [B]}$

Gödel használta először a modális operátort bizonyíthatósági interpretációban, mikor 1933-ban kimutatta az intuicionista logikáról, hogy lefordítható C. I. Lewis egyik modális kalkulusába - ez a rendszer S4 volt. Egy jó fordítás például az oldalt található (rekurzív) $\scriptstyle {[\cdot ]}$ függvény.

Az ehhez hasonló fordítások felfedezése jelentős volt az intuicionisták számára is, hiszen a Kripke-szemantikák felfedezése után e fordítás megléte azt is jelentette, hogy S4 (adekvát) szemantikája szemantikája az intuicionista logikának is. Az intuicionizmus szokásos Kripke-szemantikája végülis nem S4 szemantikája lett, azaz a reflexív és tranzitív keretstruktúrák, hanem a reflexív, tranzitív és antiszimmetrikus keretstruktúrák, amelyekhez közel majd egy másik bizonyíthatósági logika, a Grz rendszer áll majd közel.

Peano-Aritmetika

GL

GL lefordítása PA-ra
$\scriptstyle {[p]}$	$\scriptstyle {p}$
$\scriptstyle {[\lnot A]}$	$\scriptstyle {\lnot [A]}$
$\scriptstyle {[A\rightarrow B]}$	$\scriptstyle {[A]\rightarrow [B]}$
$\scriptstyle {[A\vee B]}$	$\scriptstyle {[A]\vee [B]}$
$\scriptstyle {[A\land B]}$	$\scriptstyle {[A]\land [B]}$
$\scriptstyle {[\Box A]}$	$\scriptstyle {Lev\,(\ulcorner [A]\urcorner )}$

A legfontosabb bizonyíthatósági modális rendszer, a GL rendszer (Gödel és Löb után) melyre a Kripke-féle (keretstruktúrás) szemantikán kívül egy alternatív szemantika is adható. Ez az alternatív - egyébként helyes és teljes - szemantika egy a Peano-aritmetika nyelvére való fordítás. A fordítás a $\scriptstyle {\Box }$-okhoz a Gödel számozást és a bizonyíthatósági predikátumot használja fel. Az oldalt látható táblázat megadja ezt a bizonyos szemantikát. A $\scriptstyle {PA\vdash \sigma }$ jelölés azt jelenti, hogy a $\scriptstyle {\sigma }$ aritmetikai formula levezethető $\scriptstyle {PA}$-ból. Erről Gödel munkássága óta tudjuk, hogy ennek egy árnyéka, vetülete megjelenik $\scriptstyle {PA}$ nyelvében magában is: Vezessük be először is a $\scriptstyle {\ulcorner \sigma \urcorner }$ függvényjelet. Ez egy trükkös módszerrel (lásd: Gödel-számozás) számokat rendel minden formulához. Ezt követően bevezetünk majd egy predikátumot, $\scriptstyle {Lev}$-et, amit a következőképpen definiálunk:

Ez a predikátum akkor és csak akkor legyen igaz, ha ez a $\scriptstyle {\sigma }$ aritmetikai formula gödel-száma levezethető $\scriptstyle {PA}$-ból

Azaz:

$\scriptstyle {Lev\,(\ulcorner \sigma \urcorner )\quad \iff \quad PA\vdash \sigma }$

Ekkor a Gödel-tétel értelmében a következő - modális formuláink konstrukciójához hasonló konstrukcióval bíró - formulákra bukkanhatunk beszédünkben, miközben $\scriptstyle {PA\vdash \sigma }$-ról tettünk a fenti módszerrel megállapításokat.

• Ha $\scriptstyle {PA\vdash \sigma }$, akkor $\scriptstyle {PA\vdash Lev\,(\ulcorner \sigma \urcorner )}$ is.
• $\scriptstyle {Lev\,(\ulcorner \sigma \rightarrow \tau \urcorner )\rightarrow (Lev\,(\ulcorner \sigma \urcorner )\rightarrow Lev\,(\ulcorner \tau \urcorner ))}$
• $\scriptstyle {Lev\,(\ulcorner \sigma \urcorner )\rightarrow Lev\,(\ulcorner Lev\,(\ulcorner \sigma \urcorner )\urcorner )}$
• $\scriptstyle {Lev\,(\ulcorner Lev\,(\ulcorner \sigma \urcorner )\rightarrow \sigma \urcorner )\rightarrow Lev(\ulcorner \sigma \urcorner })$

Azaz, a könnyebb áttekinthetőség érdekében a $\scriptstyle {Lev\,(\ulcorner \cdot \urcorner )}$ helyébe $\scriptstyle {\Box }$-ot írva:

• Modális generalizáció: Ha $\scriptstyle {PA\vdash A}$, akkor $\scriptstyle {PA\vdash \Box A}$ is.
• K: $\scriptstyle {\Box (A\rightarrow B)\rightarrow \Box A\rightarrow \Box B}$
• tra : $\scriptstyle {\Box A\rightarrow \Box \Box A}$
• Löb : $\scriptstyle {\Box (\Box A\rightarrow A)\rightarrow \Box A}$

A rendszer néhány érdekessége:

• Az alternatívareláció irreflexív. (Az olyan keretstruktúraosztály, amely pontosan az irreflexív keretstruktúrákat tartalmazza, modálisan definiálhatatlan. A GL azonban erősebb rendszer így lehetséges, hogy minden modellje irreflexív.)
• A hozzá tartozó keretstruktúrák pontosan azok, amelyek tranzitívak és inverz jólfundáltak. Ez utóbbi a következő (ekvivalens kijelentéseket) jelenti:
  • $\scriptstyle {R^{-1}}$ jólrendezett,
  • nincsen $\scriptstyle {R}$ szerint felszálló végtelen lánc.
  • nincsenek $\scriptstyle {w_{1},w_{2},w_{3}...}$ világok, hogy $\scriptstyle {...w_{3}Rw_{2}Rw_{1}}$

    $\scriptstyle {\forall P\exists x(Px\land \forall y(Py\rightarrow (\lnot x=y\rightarrow yRx)))}$

Ez utóbbi különösen azért érdekes, mert ez a tulajdonság elsőrendben már egyáltalán nem megfogalmazható. E tulajdonság az, ami miatt irreflexívek ugyanezen keretstruktúrák.

• $\scriptstyle {\Box A\rightarrow A}$ nem tétele, de ez az előbbi tulajdonságból is következik.
• Nincsenek $\scriptstyle {\Diamond A}$ formájú tételei. Mint például a $\scriptstyle {\lnot \Box \lnot \top }$, azaz $\scriptstyle {\lnot \Box \bot }$. Ez ugyanis olyasmit jelenthetne, hogy bizonyítható lenne, hogy a 0=1 állítás nem bizonyítható -- ez pedig szó szerint az aritmetika ellentmondásmentességének bizonyítása, ami a II. Gödel tétel értelmében nem lehetséges.
• $\scriptstyle {\top }$ tekintetében még a $\scriptstyle {\Box \Diamond \top }$ sem tétele GL-nek.
• $\scriptstyle {\Box \bot \leftrightarrow \Box \Diamond \top }$ viszont tétel.
• Viszont valahányszor tétele GL-nek egy $\scriptstyle {\Box A\rightarrow A}$ formula, annyiszor tétele $\scriptstyle {A}$ maga is. Ez Löb tételével cseng össze.

Honnan a Löb formula? - A részletezés jobbra nyitható!

Minden $\scriptstyle {PA}$-beli formulának vannak fix pontjai: olyan $\scriptstyle {\sigma }$ mondatok, melyekre a diagonalizációs lemma alapján fennáll: $\scriptstyle {PA\,\vdash \,\sigma \,\,\leftrightarrow \,\,F\,(\ulcorner \sigma \urcorner )}$.

A $\scriptstyle {Lev}$ predikátum fixpontja ez alapján: $\scriptstyle {PA\,\vdash \,\sigma \,\,\leftrightarrow \,\,Lev\,(\ulcorner \sigma \urcorner )}$.

Arra a kérdésre, hogy vajon bizonyítható-e ez, Löb adott egy választ (ez lenne Löb tétele): Ha $\scriptstyle {PA\,\vdash \,Lev\,(\ulcorner \sigma \urcorner )\,\,\rightarrow \,\,\sigma }$, akkor $\scriptstyle {PA\,\vdash \,\sigma }$.

Ez utóbbit $\scriptstyle {PA}$ nyelvére átírva megkapjuk a W axiómát vagy Löb formulát:

Löb: $\scriptstyle {Lev\,(\ulcorner Lev\,(\ulcorner \sigma \urcorner )\rightarrow \sigma \urcorner )\rightarrow Lev(\ulcorner \sigma )\urcorner \quad }$,

Löb: $\scriptstyle {\quad \Box (\Box A\rightarrow A)\rightarrow \Box A}$

A GL kalkulus - Jobbra nyithatod ki a táblázatokat!

A GL kalkulus
Axiómák	Klasszikus	(A1)	$\scriptstyle {A\rightarrow (B\rightarrow A)}$
		(A2)	$\scriptstyle {(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))}$
		(A3)	$\scriptstyle {((\lnot A)\rightarrow (\lnot B))\rightarrow (B\rightarrow A)}$
	Modális	K	$\scriptstyle {\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}$
		Löb	$\scriptstyle {\Box (\Box A\rightarrow A)\rightarrow \Box A}$
Levezetési szabályok:	Klasszikus	(MP)	$\scriptstyle {\frac {A,A\rightarrow B}{B}}$
	Modális	(MG)	$\scriptstyle {\frac {A}{\Box A}}$

Egy másik, sokkal fontosabb és érdekesebb bizonyíthatósági kalkulus a GL (Gödel és Löb után). Itt az állítások a Peano-aritmetika bizonyíthatóságára van illesztve. Bár ennek a Kripke-modelljei tranzitívak, nem feltétlen szükséges az ezt biztosító tra axióma -- ez ugyanis levezethető a GL kódú axiómából, ami a következő:

$\scriptstyle {\Box (\Box A\rightarrow B)\rightarrow \Box A}$

Ez az axióma Löb tételének felel meg.

Forrás

• szerk.: Solomon Feferman: Collected Works (angol, német nyelven). Oxford: Oxford University Press. ISBN 0-19-503964-5 (1986) 
• George Boolos. The Logic of Provability. New York: Cambridge University Press (1993). ISBN 0-521-48325-5 

Külső hivatkozások

• Sergei N. Artemov, Lev. D. Beklemishev. Provability Logic (angol nyelven), 174. o.