Logikai kalkulus

Logikai kalkuluson olyan adott nyelv formuláihoz tartozó formális rendszert, szabályrendszert értünk, amely pusztán szintaktikailag, szemantika nélkül ad meg egy következményrelációt. A logikai kalkulus tehát egy axiómarendszer, amely magában a logikai tautológiákat állítja elő, adott formulákat ideiglenesen hozzávéve (premissza) pedig más formulákra (konklúzió) lehet jutni (következtetni) vele.

Tehát például a klasszikus logika esetében, ha rendelkezünk egy alkalmas logikai kalkulussal, akkor anélkül tudunk számot adni a szokásos következmény, logikai igazság, ellentmondás és ekvivalencia, és általában a logikai konstansok fogalmáról, hogy az „igaz” és „hamis” szavak, azaz a szemantika segítségére szorulnánk.

Logikai kalkulusról általában

Mivel a logikai kalkulus a szintaxisban kísérel meg definiálni minden szokásos logikai fogalmat, ezért minden esetleg máshonnan ismert logikai kifejezésnek, mint például a „logikai igazság”-nak lesz egy kalkulusos megfelelője. Ezen a fogalmak definíciójában csak és kizárólag szintaktikai fogalmak szerepelnek majd, mint például „formula”, „formulaséma”, „formulasorozat”.

Logikai igazságok

A logikai kalkulus egy olyan szintaktikai induktív (rekurzív) definíció, amely egy nyelv formulái halmazán belül elkülöníti, definiálja a logikai igazságokat. Általában ezt úgy teszi, hogy megad néhány formulát, amelyet logikai igazságnak (vagy más szóval tételnek, tautológiának) posztulál, majd megad egy vagy több bővítési (más szóval levezetési, következtetési, derivációs) szabályt, amellyel a meglévő tételekből új tételeket lehet előállítani.

Azt, hogy egy $\scriptstyle A$ formula vagy formulaséma logikai igazság, a következőképpen jelöljük:

$\scriptstyle \vdash A$

Premisszák és konklúziók

Általában azonban nem csak a logikai igazságok meghatározására használják a kalkulust, hanem a következményreláció meghatározására is. Ez azt jelenti, hogy a kalkulus vizsgálatakor arról is számot adunk, hogy a meglévő axiómákhoz és levezetési szabályokhoz új formulákat hozzávéve milyen más formulák levezetésére vagyunk képesek. Ezeket az ideiglenesen felvett formulákat nevezzük premisszáknak, és azt, amit így le tudtunk vezetni, nevezzük konklúziónak.

Azt, hogy egy $\scriptstyle A$ formulából vagy formulasémából (premisszából) levezethető egy $\scriptstyle B$ formula vagy formulaséma (konklúzió), a következőképpen jelöljük:

$\scriptstyle A\vdash B$

A premisszák helyén azonban gyakran vannak premisszahalmazok, vagy premisszasorozatok. Ez azzal egyenértékű, hogy több premisszát is felhasználunk. Ha $\scriptstyle \Gamma =\{A_{1},,A_{2}\dots \}$ véges vagy végtelen formulahalmaz vagy $\scriptstyle \Gamma =A_{1},A_{2},\dots$ egy formulasorozat, akkor azt, hogy $\scriptstyle \Gamma$-ból levezethető egy $\scriptstyle A$ állítás, a következőképpen jelöljük:

$\scriptstyle \Gamma \vdash A$

Ennek megfelelően az, hogy egy $\scriptstyle A$ formula logikai igazság, azzal egyenértékű, hogy üres premisszahalmazból is levezethető.

A Gentzen-féle szekvenskalkulusban előfordul az is, hogy a formulasorozatok is léphetnek fel konklúziószerepben. Ekkor ha $\scriptstyle \Gamma$ és $\scriptstyle \Delta$ két ilyen formulasorozat, akkor

$\scriptstyle \Gamma \vdash \Delta$

intuitíve azt jelenti, hogy $\scriptstyle \Gamma$-beli formulák konjunkciójából levezethető a $\scriptstyle \Delta$-beli formulák diszjunkciója, azaz $\scriptstyle \Delta$ egyik, vagy másik, vagy' harmadik stb. formulája.

Centrális logikai fogalmak

• Konzisztens egy kalkulus vagy formulahalmaz, ha belőle nem vezethető le a nyelv összes formulája. Más szóval a kalkulus, mint definíció, nem a nyelvet határozza meg. Ez a logikai kalkulusok esetében egyenértékű azzal, hogy a formulahalmazból nem vezethető le ellentmondás, így ezáltal is szokás definiálni a konzisztencia fogalmát. Ez felel meg a kielégíthetőség szemantikai fogalomnak.

Inkonzisztens egy kalkulus, ha nem konzisztens. Ez felel meg az ellentmondásos szemantikai fogalomnak.

• A következményreláció nem más, mint az induktívan definiált $\scriptstyle \vdash$ jel. Általában pedig a $\scriptstyle \Gamma \vdash A$ azt jelenti, hogy az $\scriptstyle A$ formula vagy formulaséma megkapható a logikai kalkulus axiómáiból és a $\scriptstyle \Gamma$ premisszahalmaz formuláiból a kalkulus bővítési szabályainak véges sokszori alkalmazásával.
• Az ekvivalencia fogalmát a következményviszony fogalmára vezetjük vissza. $\scriptstyle A$ és $\scriptstyle B$ szintaktikailag ekvivelensek, ha $\scriptstyle A\vdash B$ és $\scriptstyle B\vdash A$.

Ezt néha a következőképpen jelölik: $\scriptstyle A\dashv \vdash B$

Helyesség, teljesség, adekvátság

Egy adott nyelv esetén mindig felmerül a kérdés, hogy hogyan illik egymáshoz a kalkulus és a szemantika, azaz a kettő által definiált fogalmak milyen viszonyban állnak egymással. Jelölje a szemantikai következményrelációt $\scriptstyle \vDash$.

• A $\scriptstyle \vdash$-t meghatározó kalkulus helyes a $\scriptstyle \vDash$-t meghatározó szemantikára nézve, ha

$\scriptstyle \Gamma \vdash A$-ból következik $\scriptstyle \Gamma \vDash A$. Ilyen például egy intuicionista kalkulus egy klasszikus szemantikára nézve.

• A $\scriptstyle \vdash$-t meghatározó kalkulus teljes a $\scriptstyle \vDash$-t meghatározó szemantikára nézve, ha

$\scriptstyle \Gamma \vDash A$-ból következik $\scriptstyle \Gamma \vdash A$. Ilyen például egy inkonzisztens kalkulus bármilyen szemantikára nézve.

• * A $\scriptstyle \vdash$-t meghatározó kalkulus adekvát a $\scriptstyle \vDash$-t meghatározó szemantikára nézve, ha helyes és teljes, azaz ha

$\scriptstyle \Gamma \vdash A$ akkor és csak akkor, ha $\scriptstyle \Gamma \vDash A$.

Adekvát kalkulusok létezése

Nem minden logikához szerkeszthető adekvát logikai kalkulus. Klasszikus nulladrendű és elsőrendű logikához, intuicionista nulladrendű és elsőrendű logikához, a nulladrendű modális logikákhoz, a legtöbb standard modális elsőrendű logikához adható logikai kalkulus, azonban például a másodrendű klasszikus logika nem axiomatizálható.

Kalkulusok típusai

Frege-Hilbert típusú kalkulus

Egy Frege-Hilbert kalkulus egy vagy több levezetési szabályból és több axiómából vagy axiómasémából áll. Legfőbb jellemzője a takarékosság; a lehető legtömörebben vannak kifejtve, lehetőség szerint mellőznek minden redundanciát. A legtöbb esetben mindig csak egy-két logikai konstans szerepel bennük, a többit pedig definíció alapján vezetik be.

Klasszikus logika kalkulusai

A klasszikus logikának sokféle axiomatizálása van. A két következő kalkulus végső soron Fregétől, Hilberttől, Łukasiewitz-től ered, mi Ruzsa Imre megfogalmazásában közöljük:

Nulladrendű kalkulus Axiómasémák (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)}$ Levezetési szabályok: (MP) $\scriptstyle {\frac {A,A\rightarrow B}{B}}$

Elsőrendű kalkulus Axiómasémák (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)}$ (A4) $\scriptstyle {(\forall xA\rightarrow A_{x}^{t})}$ (A5) $\scriptstyle {(\forall x(A\rightarrow B)\rightarrow (\forall xA\rightarrow \forall xB))}$ (A6) $\scriptstyle {(A\rightarrow \forall xA)}$ Levezetési szabályok: (MP) $\scriptstyle {\frac {A,A\rightarrow B}{B}}$

Itt az elsőrendű kalkulusnál fontos, hogy az (A6) axiómánál $\scriptstyle A$-ban $\scriptstyle x$-nek nincs szabad előfordulása. Szokás még ezt a formulát levezetési szabályként felvenni ugyanezen kikötéssel:

$\scriptstyle {\frac {A}{\forall xA}}$

Ennek a szabálynak a neve univerzális generalizáció, jele pedig (UG).

Szokás még nem axiómasémákkal (azaz végtelen sok axiómával) megadni kalkulust, hanem véges sok formulaváltozóval, amelyeket egy formulabehelyettesítés nevezetű levezetési szabállyal változtatnak formulává. Ez esetben két levezetési szabály van három axiómára, nem pedig egy levezetési szabály végtelen sok axiómára, a végeredmény azonban gyakorlatilag ugyanaz.

A klasszikus logikai kalkulusok adekvátak a szokásos megfelelő szemantikákra nézve.

Az intuicionista logika kalkulusai

Nulladrendű kalkulus Axiómasémák (A1) $\scriptstyle {A\rightarrow (B\rightarrow A)}$ (A2) $\scriptstyle {(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))}$ (A3) $\scriptstyle {((A\land B)\rightarrow A}$ (A4) $\scriptstyle {((A\land B)\rightarrow B}$ (A5) $\scriptstyle {(A\rightarrow (B\rightarrow (A\land B)))}$ (A6) $\scriptstyle {(A\rightarrow (A\lor B)))}$ (A7) $\scriptstyle {(B\rightarrow (A\lor B)))}$ (A8) $\scriptstyle {((A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow ((A\lor B)\rightarrow C)))}$ (A9) $\scriptstyle {(\bot \rightarrow A)}$ Levezetési szabályok: (MP) $\scriptstyle {\frac {A,A\rightarrow B}{B}}$

Elsőrendű kalkulus Axiómasémák (A1) $\scriptstyle {A\rightarrow (B\rightarrow A)}$ (A2) $\scriptstyle {(A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))}$ (A3) $\scriptstyle {((A\land B)\rightarrow A}$ (A4) $\scriptstyle {((A\land B)\rightarrow B}$ (A5) $\scriptstyle {(A\rightarrow (B\rightarrow (A\land B)))}$ (A6) $\scriptstyle {(A\rightarrow (A\lor B)))}$ (A7) $\scriptstyle {(B\rightarrow (A\lor B)))}$ (A8) $\scriptstyle {((A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow ((A\lor B)\rightarrow C)))}$ (A9) $\scriptstyle {(\bot \rightarrow A)}$ (A10) $\scriptstyle {(\forall xA(x)\rightarrow A(t))}$ (A11) $\scriptstyle {(A(t)\rightarrow \exists xA(x))}$ Levezetési szabályok: (MP) $\scriptstyle {\frac {A,A\rightarrow B}{B}}$ (UG) $\scriptstyle {\frac {A\rightarrow B}{A\rightarrow \forall xB}}$ (EG) $\scriptstyle {\frac {A\rightarrow B}{\exists xA\rightarrow B}}$

Itt az elsőrendű esetnél az egzisztenciális (EG) és univerzális generalizációnál (UG) nem lehet $\scriptstyle x$-nek $\scriptstyle B$-ben szabad előfordulása, továbbá (A10)-nél és (A11)-nél a $\scriptstyle t$ terminus szabad $\scriptstyle x$-re nézve.

Ebben azért van sokkal több axióma, mivel a logikai konstansok nem definiálhatók egymással, mint a klasszikus logikában, így külön axiómák szükségesek mindegyik logikai konstansra. Az axiómák egyébként a természetes levezetés megfelelő szabályai lefordítva a Frege-Hilbert-féle stílusra.

Az intuicionista logikai kalkulusok adekvátak a megfelelő (például Kripke-)szemantikákra nézve.

Az modális logika kalkulusai

A modális kalkulusok mindig a klasszikus logika néhány modális jeleket tartalmazó axiómával és modális generalizáció levezetési szabályával való bővítései.

Természetes levezetés

A természetes levezetés legfőbb jellemzője, hogy nincsenek axiómái vagy axiómasémái, csak levezetési szabályai, azokból azonban több is. A levezetési szabályok a logikai konstansok használatát írják le, ebből fakadóan jellemzően intuicionista kalkulusról van szó.

Gentzen típusú szekvenskalkulus

Ebben a kalkulusban nem formulákra vonatkoznak a szabályok és nem is formulák alkotják az axiómákat, hanem a formulák eddigi szerepét az ún. szekvensek töltik be. Szekvensnek nevezzük a

$\scriptstyle \Gamma \vdash \Delta$

alakú jelsorozatokat, ahol $\scriptstyle \Gamma$ és $\scriptstyle \Delta$ olyan rendezett jelsorozatok, amelyeknek minden tagja egy formula. A $\scriptstyle \vdash$ bal oldalán lévő formulákat „és”-sel érdemes kiolvasni, a jobb oldalán lévő formulákat pedig „vagy”-gyal. Tehát

$\scriptstyle A,B,C\vdash A,D$

kiolvasva:

$\scriptstyle A$-ból $\scriptstyle B$-ből és $\scriptstyle C$-ből együtt következik $\scriptstyle A$ vagy $\scriptstyle D$

Irodalom

• Ruzsa Imre. Logikai szintaxis és szemantika I. (magyar nyelven). Budapest: Akadémiai Kiadó. ISBN 963-05-4720-1 (1988) 
• Alexander Chagrov – Michael Zakharyaschev. Modal Logic. Oxford: Clarendon Press. ISBN 9780198537793 (1997) 
• Ruzsa, Imre, Máté András. Bevezetés a modern logikába. Budapest: Osiris Kiadó. ISBN 963-379-185-5 (1997) 
• Pásztorné Varga Katalin - Várterész Magda. A matematikai logika alkalmazásszemléletű tárgyalása. Budapest: Panem Könyvkiadó. ISBN 963-545-364-7 (2003) 
• Gentzen, Gerhard (1935). Untersuchungen über das logische Schliessen. Mathematische Zeitschrift 39. No. 1, 176-210. o. DOI:10.1007/BF01201353. 1432-1823. (Hozzáférés: 2010. július 9.)  
• Dirk van Dalen (2001). „Intuitionistic Logic”. Handbook of Philosophical Logic 5, Kiadó: Springer. ISBN 0792371607.  

Külső hivatkozások

• Csirmaz, László & Hajnal, András: Matematikai logika egyetemi jegyzet, ELTE Bp, 1994 (Postscript változat)