Bizonyíthatósági logika

A Wikipédiából, a szabad enciklopédiából

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 \scriptstyle{\Box } 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[szerkesztés | forrásszöveg szerkesztése]

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 nyelf 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[szerkesztés | forrásszöveg szerkesztése]

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 \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 kapott modális formulát „\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 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 \scriptstyle{w_1} tudásállapot kibővíthető egy \scriptstyle{w_2}-vé, ami pedig egy \scriptstyle{w_3}-má, akkor \scriptstyle{w_1} is kibővíthető \scriptstyle{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 \scriptstyle{\Box A} egy \scriptstyle{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.

Exclmid.PNG

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 tudásállapotban hamis a \scriptstyle{p}, 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.

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[szerkesztés | forrásszöveg szerkesztése]

A Peano-aritmetika egy fordítása úgy néz ki, hogy a Peano-aritmetikában szereplő azon \scriptstyle{Bew} predikátumot, mely a levezethetőséget kódolja, írjuk át \scriptstyle \Box -ra. Mivel \scriptstyle{Bew} a Peano-aritmetikában lévő levezethetőségnek felel meg, így \scriptstyle \Box 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:

\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 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[szerkesztés | forrásszöveg szerkesztése]

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ő \scriptstyle \Box 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 \scriptstyle{\Box (\Box bot \rightarrow \bot) } formula. Mivel egy formális rendszerben bizonyítható \scriptstyle{\top}, \scriptstyle{\sim \Box \bot} 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 \scriptstyle \exists x Bew(x,y) bizonyíthatóságról szóló predikátumot. Ezt a \scriptstyle Bew(x,y) predikátumot akkor tekintenénk igaznak, ha \scriptstyle x bizonyítása lenne \scriptstyle y-nak, ahol is egy Peano-aritmetikát tartalmazó formális rendszerben \scriptstyle y lehetne a kérdéses formula Gödel-száma, \scriptstyle 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[szerkesztés | forrásszöveg szerkesztése]

Modális logikák intuicionista logikára[szerkesztés | forrásszöveg szerkesztése]

S4[szerkesztés | forrásszöveg szerkesztése]

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.[1] Egy jó fordítás például az oldalt található (rekurzív) \scriptstyle{[\cdot ]} függvény, melyet szokás Gödel-fordításnak is nevezni[2]. Ez szemléletesen szólva annyit tesz, hogy minden atomi formula és negációjel elé elhelyez egy \scriptstyle \Box jelet. Van azonban több lehetséges fordítás is, pl. hogy minden részformulát ellátunk egy \scriptstyle \Box 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:

  • \scriptstyle \lnot A \quad \rightsquigarrow \quad \scriptstyle \Box \lnot A szemléletes jelentése: Innentől mindig tudjuk majd, hogy \scriptstyle 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[szerkesztés | forrásszöveg szerkesztése]

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

Grz \scriptstyle \Box(\Box (p \to \Box p)\rightarrow p)\rightarrow p

formulát vesszük fel. Ebből az axiómából levezethetők S4 axiómái, azaz \scriptstyle \Box p\rightarrow p és \scriptstyle \Box p \to \Box \Box p)\rightarrow 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 \scriptstyle w_1 Rw_2Rw_3R\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[szerkesztés | forrásszöveg szerkesztése]

A Peano-aritmetika modális kalkulusai[szerkesztés | forrásszöveg szerkesztése]

GL[szerkesztés | forrásszöveg szerkesztése]

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)}

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 \scriptstyle{\Box}-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 \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 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, \scriptstyle{Biz}-t, 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:

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 \scriptstyle{PA}-beli formulának vannak ún. fix pontjai, azaz olyan \scriptstyle{  \sigma} mondatok, melyekre a diagonalizációs lemma alapján fennáll: \scriptstyle{PA\,\vdash \,\sigma \,\, \leftrightarrow\,\, F\, (\ulcorner \sigma \urcorner )}. Mármost a \scriptstyle{Lev} predikátum fixpontja ez alapján: \scriptstyle{ PA \,\vdash \,\sigma \,\,\leftrightarrow \,\,Lev\,(\ulcorner \sigma \urcorner )}. 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 \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 Löb formulának megfelelő számelméleti állítást:
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 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[3]:

  • Az alternatívareláció irreflexív lesz.[4]
  • 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_3Rw_2Rw_1}
      \scriptstyle{ \forall P \exists x (Px \land \forall y (Py \rightarrow (\lnot x=y \rightarrow yRx ))) }
  • \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ás-mentessé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.

GLS[szerkesztés | forrásszöveg szerkesztése]

Forrás[szerkesztés | forrásszöveg szerkesztése]

  • 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[szerkesztés | forrásszöveg szerkesztése]

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

Jegyzetek[szerkesztés | forrásszöveg szerkesztése]

  1. Solomon Feferman Kurt Gödel Collected Works, i. m. 1 kötet, 2 fejezet, 296. old.
  2. Szokás még használni a Gödel-Tarski-McKinsey fordítás elnevezést is.
  3. Boolos 1993 p. xvii.
  4. Az olyan keretstruktúra-osztá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.