Bizonyíthatósági logika

A bizonyíthatósági logika a modális logika egyik 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 $◻$ jellel szokás jelölni, és leggyakrabban „boksz”-nak szokás mondani.

A bizonyíthatósági logika megjelenését Kurt Gödel egy 1933-as cikkéhez szokás kapcsolni, melyben egy modális logika és az intuicionista logika kapcsolatával foglalkozik. A bizonyíthatósági logika leghíresebb eredményét, mely arról szólt, hogy a Peano-aritmetika bizonyíthatóság-fogalma pontosan megragadható egy modális logikával, Robert Martin Solovay publikálta 1976-ban.

Példák

Mikor egy formális rendszerben a bizonyíthatóság fogalmát egy modális logikával szándékozzuk megragadni, szükség van egy szótárra, ami a két nyelv formuláit valamilyen módon megfelelteti egymásnak. Fordításnak nevezzük és keretes zárójelekkel jelöljük majd azt a függvényt, amely a két nyelv formulái közt a kapcsolatot megteremti.

Az alábbiakban szerepel a két leghíresebb, fenti bevezetőben is említett fordításokkal egy-egy példa. Az első példában modális logikára, a másodikban modális logikából való fordításra szerepel példa, azonban mindkét fordítás fordított irányba is tökéletesen működik (ezen megállapítások bizonyításai számítanak a terület fő eredményeinek.)

Intuicionista logika

Az intuicionista logikánál az egyik alkalmas fordítás szerint, amely az ún. S4 modális logikába fordít, minden atomi mondat és negációjel elé egy $◻$-ot kell írni, így pl. egy, a kizárt harmadik elvét képviselő formula a következő alakot ölti:

$p\vee \mathrm{\neg }p⇝◻p\vee ◻\mathrm{\neg }◻p$

Szóban mondva a kapott modális formulát „$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 szemantikája alapján S4-re a következő szemantika áll a rendelkezésünkre: A lehetséges világok különböző tudásállapotoknak felelnek meg, melyek egymással olyan módon kapcsolódnak össze, hogy az egyik tudásállapot információi kibővíthetők-e a másik tudásállapot információivá. Ez alapján ez az ún. alternatívareláció egy előrendezésnek felel meg, azaz

• reflexív, azaz minden tudásállapot (triviális) bővítése a saját információinak
• tranzitív, azaz ha egy $w_1$ tudásállapot kibővíthető egy $w_2$-vé, ami pedig egy $w_3$-má, akkor $w_1$ is kibővíthető $w_3$-má.

A bizonyíthatóság ide pedig úgy kapcsolódik, hogy, ha valamit bebizonyítottunk, akkor azt mindörökké tudni fogjuk; minden későbbi tudásállapotban ott lesz. Eszerint $◻A$ egy $w$ tudásállapotban akkor és csak akkor szerepel, vagy más szóval igaz, ha minden későbbi, ebből kibővítve kapott tudásállapotban is igaz.

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 $◻p\vee ◻\mathrm{\neg }◻p$ formula, akkor ez valóban hamis lesz, mivel egyrészt $◻p$ valóban nem igaz, hiszen a bal oldali tudásállapotban hamis a $p$, másrészt pedig $◻\mathrm{\neg }◻p$ sem igaz, mivel a jobb oldali világnak minden rákövetkezőjében (azaz önmagában) igaz a $p$.

A szemantika szemszögéből tehát azt mondhatjuk, hogy az S4 kalkulusnak két (adekvát) szemantikája is 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 $Bew$ predikátumot, mely a levezethetőséget kódolja, írjuk át $◻$-ra. Mivel $Bew$ a Peano-aritmetikában lévő levezethetőségnek felel meg, így $◻$ rajta keresztül 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 nézzük a következő formulát:

$◻\mathrm{\neg }◻\mathrm{\perp }⇝Lev(⌜\mathrm{\neg }Lev(⌜0=1⌝)⌝)$

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 a második nemteljességi tétel á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 a Peano-aritmetika.

A kutatás két iránya

A bizonyíthatósági logika ötlete Gödeltől származik, amikor 1933-ban megfogalmazott egy fordítást a nulladrendű intuicionista kalkulus és C.I. Lewis S4 modális kalkulusa közt. Gödel ugyanakkor még ebben a cikkben leszögezte, hogy az S4-ben szereplő $◻$ nem jelentheti általában véve egy formális rendszerben a bizonyíthatóságot, mivel a kalkulusnak tételei olyan formulák, melyek ilyen módon interpretálva az aritmetikát tartalmazó formális rendszerekben ellent mondanának a Gödel-féle nemteljességi tételeknek. Ilyen például az S4-beli $◻(◻bot\to \mathrm{\perp })$ formula. Mivel egy formális rendszerben bizonyítható $\mathrm{\top }$, $\sim ◻\mathrm{\perp }$ is bizonyítható lenne, ami nem mást jelent, mint hogy nem bizonyítható az ellentmondás - ez pedig a konzisztenciát jelentené, ami az aritmetikát tartalmazó rendszerekben nem bizonyítható.

Innen indulva a bizonyíthatósági logikának két fő területe van:

1. Megadni a bizonyíthatóság logikáját, azaz megadni azt a modális logikát, amely egy adott formális rendszerben leírja a $\mathrm{\exists }xBew(x,y)$ bizonyíthatóságról szóló predikátumot. Ezt a $Bew(x,y)$ predikátumot akkor tekintenénk igaznak, ha $x$ bizonyítása lenne $y$-nak, ahol is egy Peano-aritmetikát tartalmazó formális rendszerben $y$ lehetne a kérdéses formula Gödel-száma, $x$ pedig a hozzá vezető bizonyítás (formulasorozat) Gödel-száma. Ebben az esetben tehát egy meglévő modellhez keresünk kalkulust.
2. Megadni a bizonyítások logikáját, azaz a meglévő, konstruktív bizonyításokat elviekben jól leíró S4 kalkulusra, és így az IPC kalkulusra egy bizonyításokkal kapcsolatos szemantikát.

A bizonyítások logikája

Modális logikák intuicionista logikára

S4

IPC lefordítása S4-re
$[p]$	$◻p$
$[\mathrm{\neg }A]$	$◻\mathrm{\neg }[A]$
$[A\to B]$	$[A]\to [B]$
$[A\vee B]$	$[A]\vee [B]$
$[A\wedge B]$	$[A]\wedge [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) $[\cdot ]$ függvény, melyet szokás Gödel-fordításnak is nevezni. Ez szemléletesen szólva annyit tesz, hogy minden atomi formula és negációjel elé elhelyez egy $◻$ jelet. Van azonban több lehetséges fordítás is, pl. hogy minden részformulát ellátunk egy $◻$ jellel.

S4 modelljei a reflexív és tranzitív keretstruktúrák (lásd: Modális logika). Itt a lehetséges világok episztemikus állapotokat jelölnek. A fordítás során pl. az intuicionista negáció szerepére a következőképpen lehet a S4 modális szemantikájának ismeretében rávilágítani:

• $\mathrm{\neg }A⇝◻\mathrm{\neg }A$ szemléletes jelentése: Innentől mindig tudjuk majd, hogy $A$ hamis.

Nem az S4 modális kalkulus az egyetlen modális kalkulus, amelybe a nulladrendű intuicionista logikát be lehet ágyazni, azonban bizonyítható, hogy ez a leggyengébb ilyen kalkulus. A legerősebb ezek közül a Grz.

Grz

Ezt a modális kalkulust úgy kaphatjuk a K normális modális rendszerből, hogy egyetlen axiómaként az

Grz $◻(◻(p\to ◻p)\to p)\to p$

formulát vesszük fel. Ebből az axiómából levezethetők S4 axiómái, azaz $◻p\to p$ és $◻p\to ◻◻p)\to p$.

Grz Kripke modelljei azon keretstruktúrák lesznek, melyek reflexívek, tranzitívak, és nincsen bennük végtelen szigorúan felszálló ág. Ez utóbbi egy olyan elsőrendben nem definiálható tulajdonság, mely a következő egymással ekvivalens állításokat jelenti:

• A világok halmazának bármely részhalmazában lesz egy olyan elem, amelynek csak önmaga a rákövetkezője.
• Ha van olyan véletlen sorozat, hogy $w_{1}R{w}_{2}R{w}_{3}R\dots$, akkor ebben egy ponttól kezdve mindenhol ugyanaz a világ szerepel.

Ezekből már következik az (önmagában modálisan nem definiálható) antiszimmetria is, azaz Grz modelljei speciális parciális rendezések lesznek.

A bizonyíthatóság logikája

A Peano-aritmetika modális kalkulusai

GL

GL lefordítása PA-ra
$[p]$	$p$
$[\mathrm{\neg }A]$	$\mathrm{\neg }[A]$
$[A\to B]$	$[A]\to [B]$
$[A\vee B]$	$[A]\vee [B]$
$[A\wedge B]$	$[A]\wedge [B]$
$[◻A]$	$Lev(⌜[A]⌝)$

Az egyik 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 $◻$-okhoz a Gödel-számozást és a bizonyíthatósági predikátumot használja fel.

Bizonyíthatóság-predikátum

A $PA⊢\sigma$ jelölés azt jelenti, hogy a $\sigma$ aritmetikai formula levezethető $PA$-ból. Erről Gödel munkássága óta tudjuk, hogy ennek egy árnyéka, vetülete megjelenik $PA$ nyelvében magában is: Vezessük be először is a $⌜\sigma ⌝$ függvényjelet. Ez minden formulához és formulasorozathoz hozzárendel egy számot (lásd: Gödel-számozás). Ezáltal a Peano-aritmetika képes lesz olyan formulákat levezetni, melyek a levezetéseiről 'szólnak'. Ezt követően bevezetünk majd egy predikátumot, $Biz$-t, amit a következőképpen definiálunk:

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

Azaz:

$Lev(⌜\sigma ⌝)⟺PA⊢\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 $PA⊢\sigma$-ról tettünk a fenti módszerrel megállapításokat.

• Ha $PA⊢\sigma$, akkor $PA⊢Lev(⌜\sigma ⌝)$ is.
• $Lev(⌜\sigma \to \tau ⌝)\to (Lev(⌜\sigma ⌝)\to Lev(⌜\tau ⌝))$
• $Lev(⌜\sigma ⌝)\to Lev(⌜Lev(⌜\sigma ⌝)⌝)$
• $Lev(⌜Lev(⌜\sigma ⌝)\to \sigma ⌝)\to Lev(⌜\sigma ⌝)$

Azaz, a könnyebb áttekinthetőség érdekében a $Lev(⌜\cdot ⌝)$ helyébe $◻$-ot írva:

• Modális generalizáció: Ha $PA⊢A$, akkor $PA⊢◻A$ is.
• K: $◻(A\to B)\to ◻A\to ◻B$
• tra : $◻A\to ◻◻A$
• Löb : $◻(◻A\to A)\to ◻A$

Itt az első három jellemzőt tehát a modális generalizációt, K-t, tra-t (ami a K4 rendszert adja) szokás Hilbert–Bernays–Löb-féle levezethetőségi kritériumoknak is nevezni, mivel ezek olyan állítások, melyek egy természetes elvárást támasztanak a bizonyíthatósági predikátumunktól (és így a bizonyíthatósági modalitástól is).

Az utolsó formula Löb tételéből származik, mégpedig a következőképpen: Minden $PA$-beli formulának vannak ún. fix pontjai, azaz olyan $\sigma$ mondatok, melyekre a diagonalizációs lemma alapján fennáll: $PA⊢\sigma \leftrightarrow F(⌜\sigma ⌝)$. Mármost a $Lev$ predikátum fixpontja ez alapján: $PA⊢\sigma \leftrightarrow Lev(⌜\sigma ⌝)$. Az egyik irány az első (modális generalizálásnak megfelelő) állításból következik. Arra a kérdésre, hogy vajon a másik irány bizonyítható-e, Löb adott egy különös választ (és ez lenne Löb tétele): Ha $PA⊢Lev(⌜\sigma ⌝)\to \sigma$, akkor $PA⊢\sigma$.

Ez utóbbit $PA$ nyelvére átírva megkapjuk a Löb formulának megfelelő számelméleti állítást:

Löb: $Lev(⌜Lev(⌜\sigma ⌝)\to \sigma ⌝)\to Lev(⌜\sigma )⌝$,

Löb: $◻(◻A\to A)\to ◻A$

A GL modális logika

A GL modális logikát úgy kapjuk, hogy a K normális modális logikához hozzávesszük az utolsó Löb formulát. Ebből már következni fog a tra formula, tehát axiómarendszerként az előbbi négy megállapítás fog szerepelni.

Modális szempontból az így kapott GL logika néhány érdekessége:

• Az alternatívareláció irreflexív lesz.
• 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:
  • $R^{-1}$ jólrendezett,
  • nincsen $R$ szerint felszálló végtelen lánc.
  • nincsenek $w_1,w_2,w_3...$ világok, hogy $...w_{3}R{w}_{2}R{w}_1$

    $\mathrm{\forall }P\mathrm{\exists }x(Px\wedge \mathrm{\forall }y(Py\to (\mathrm{\neg }x=y\to yRx)))$

• $◻A\to A$ nem tétele, de ez az előbbi tulajdonságból is következik.
• Nincsenek $◊A$ formájú tételei. Mint például a $\mathrm{\neg }◻\mathrm{\neg }\mathrm{\top }$, azaz $\mathrm{\neg }◻\mathrm{\perp }$. 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ás-mentességének bizonyítása, ami a II. Gödel-tétel értelmében nem lehetséges.
• $\mathrm{\top }$ tekintetében még a $◻◊\mathrm{\top }$ sem tétele GL-nek.
• $◻\mathrm{\perp }\leftrightarrow ◻◊\mathrm{\top }$ viszont tétel.
• Viszont valahányszor tétele GL-nek egy $◻A\to A$ formula, annyiszor tétele $A$ maga is. Ez Löb tételével cseng össze.

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

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

Források

• Sablon:Cite book
• Sablon:Cite book

Külső hivatkozások

• Sablon:Cite book