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:
Szóban mondva a kapott modális formulát „ á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 tudásállapot kibővíthető egy -vé, ami pedig egy -má, akkor is kibővíthető -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 egy 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 formula, akkor ez valóban hamis lesz, mivel egyrészt valóban nem igaz, hiszen a bal oldali tudásállapotban hamis a , másrészt pedig sem igaz, mivel a jobb oldali világnak minden rákövetkezőjében (azaz önmagában) igaz a .
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 predikátumot, mely a levezethetőséget kódolja, írjuk át -ra. Mivel 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:
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 formula. Mivel egy formális rendszerben bizonyítható , 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:
- 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 bizonyíthatóságról szóló predikátumot. Ezt a predikátumot akkor tekintenénk igaznak, ha bizonyítása lenne -nak, ahol is egy Peano-aritmetikát tartalmazó formális rendszerben lehetne a kérdéses formula Gödel-száma, pedig a hozzá vezető bizonyítás (formulasorozat) Gödel-száma. Ebben az esetben tehát egy meglévő modellhez keresünk kalkulust.
- 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 | ||
---|---|---|
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) 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 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:
- szemléletes jelentése: Innentől mindig tudjuk majd, hogy 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
formulát vesszük fel. Ebből az axiómából levezethetők S4 axiómái, azaz és .
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 , 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 | ||
---|---|---|
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 jelölés azt jelenti, hogy a aritmetikai formula levezethető -ból. Erről Gödel munkássága óta tudjuk, hogy ennek egy árnyéka, vetülete megjelenik nyelvében magában is: Vezessük be először is a 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, -t, amit a következőképpen definiálunk:
Azaz:
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 -ról tettünk a fenti módszerrel megállapításokat.
- Ha , akkor is.
Azaz, a könnyebb áttekinthetőség érdekében a helyébe -ot írva:
- Modális generalizáció: Ha , akkor is.
- K:
- tra :
- Löb :
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 -beli formulának vannak ún. fix pontjai, azaz olyan mondatok, melyekre a diagonalizációs lemma alapján fennáll: . Mármost a predikátum fixpontja ez alapján: . 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 , akkor .
- Ez utóbbit nyelvére átírva megkapjuk a Löb formulának megfelelő számelméleti állítást:
- Löb: ,
- Löb:
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:
- jólrendezett,
- nincsen szerint felszálló végtelen lánc.
- nincsenek világok, hogy
- nem tétele, de ez az előbbi tulajdonságból is következik.
- Nincsenek formájú tételei. Mint például a , azaz . 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.
- tekintetében még a sem tétele GL-nek.
- viszont tétel.
- Viszont valahányszor tétele GL-nek egy formula, annyiszor tétele maga is. Ez Löb tételével cseng össze.
A GL kalkulus | |||
---|---|---|---|
Axiómák | Klasszikus | (A1) | |
(A2) | |||
(A3) | |||
Modális | K | ||
Löb | |||
Levezetési szabályok: | Klasszikus | (MP) | |
Modális | (MG) |
GLS
Források
- szerk.: Solomon Feferman: Collected Works (angol, német nyelven). Oxford: Oxford University Press (1986). ISBN 0-19-503964-5
- 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.
Jegyzetek
- ↑ Solomon Feferman Kurt Gödel Collected Works, i. m. 1 kötet, 2 fejezet, 296. o.
- ↑ Szokás még használni a Gödel-Tarski-McKinsey fordítás elnevezést is.
- ↑ Boolos 1993 p. xvii.
- ↑ 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.