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 (premissza) ideiglenesen hozzávéve 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.

A „kalkulus” kifejezést George Boole hatására egy időben a Boole-algebra jelölésére is alkalmazták, azonban ez a fajta használat mára elavult.

Logikai kalkulusról általában

A logikai kalkulusokon belül pusztán szintaktikus eszközökkel - csak a formulák felépítésére és nem azok kiértékelésére hagyatkozva - lehet definiálni a logikai fogalmakat, mégis, a szokásos logikai fogalmak legtöbbjét ezzel a látszólag korlátozott módszerrel is be lehet vezetni. Ezért minden esetleg máshonnan ismert logikai kifejezésnek, mint például a „logikai igazság”-nak, vagy a következmény-reláció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ó induktívan definiált, és szokásos rá a $\scriptstyle \vdash$ jelet használni. Á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 ekvivalensek, 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

Klasszikus Frege-Hilbert kalkulus Nulladrend 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 Axiómasémák (A4) $\scriptstyle {(\forall xA(x)\rightarrow A(t)}$ (A5) $\scriptstyle {(\forall x(A\rightarrow B)\rightarrow (\forall xA\rightarrow \forall xB))}$ Levezetési szabály: (UG) $\scriptstyle {\frac {A}{\forall xA}}$

A klasszikus logikának sokféle axiomatizálása van, az egyik legelterjedtebb a Łukasiewitztől eredő három axiómás $\scriptstyle \lnot ,\rightarrow$ jelekkel dolgozó rendszer.

Az elsőrendű kalkulusnál fontos kitétel, hogy az (UG) szabály alkalmazásakor az $\scriptstyle A$-ban $\scriptstyle x$-nek nem lehet szabad előfordulása.

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 klasszikus logikai kalkulusok adekvátak a szokásos megfelelő szemantikákra nézve.

• Példa: $\scriptstyle {\frac {\lnot \lnot A}{A}}$ levezetési szabály bizonyítása.

Eszerint ha rendelkezünk egy $\scriptstyle \lnot \lnot A$ alakú tétellel, akkor le tudjuk vezetni az $\scriptstyle A$ tételt is.

$\scriptstyle \lnot \lnot A$ Ez a feltevés.

$\scriptstyle (\lnot \lnot A\rightarrow (\lnot \lnot \lnot \lnot A\rightarrow \lnot \lnot A))$ az első axiómasémában $\scriptstyle A$-t $\scriptstyle \lnot \lnot A$-ra cseréltük, $\scriptstyle B$-t pedig $\scriptstyle \lnot \lnot \lnot \lnot A$-ra.

$\scriptstyle (\lnot \lnot \lnot \lnot A\rightarrow \lnot \lnot A)$ modus ponens

$\scriptstyle ((\lnot \lnot \lnot \lnot A\rightarrow \lnot \lnot A)\rightarrow (\lnot A\rightarrow \lnot \lnot \lnot A))$ (A3) axiómaséma, amiben $\scriptstyle A$-t $\scriptstyle \lnot \lnot \lnot A$-ra cseréltük, $\scriptstyle B$-t pedig $\scriptstyle \lnot A$-ra.

$\scriptstyle (\lnot A\rightarrow \lnot \lnot \lnot A)$ modus ponenes

$\scriptstyle ((\lnot A\rightarrow \lnot \lnot \lnot A)\rightarrow (\lnot \lnot A\rightarrow A))$ (A3) axiómaséma, amiben $\scriptstyle B$-t $\scriptstyle \lnot \lnot A$-ra cseréltük.

$\scriptstyle \lnot \lnot A\rightarrow A$ modus ponens

$\scriptstyle A$ modus ponens a feltevésből.

Ezzel a szabályt bebizonyítottuk.

Az intuicionista logika kalkulusai

Intuicionista Frege-Hilbert kalkulus Nulladrend 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 Axiómasémák (A10) $\scriptstyle {(\forall xA(x)\rightarrow A(t))}$ (A11) $\scriptstyle {(A(t)\rightarrow \exists xA(x))}$ Levezetési szabályok: (UG) $\scriptstyle {\frac {A\rightarrow B}{A\rightarrow \forall xB}}$ (EG) $\scriptstyle {\frac {A\rightarrow B}{\exists xA\rightarrow B}}$|}

Az intuicionista kalkulus elsőrendű axiómáinál a következő kikötések érvényesek:

• (A10)-nél és (A11)-nél a $\scriptstyle t$ terminus szabad $\scriptstyle x$-re nézve.
• (EG) és univerzális generalizációnál (UG) nem lehet $\scriptstyle x$-nek $\scriptstyle B$-ben szabad előfordulása,

Az intuicionista kalkulusban azért van sokkal több axióma, mert 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. Két logikai konstanst, a $\scriptstyle \leftrightarrow$ jelet azonban is rövidítésként vezetjük be, továbbá a $\scriptstyle \lnot$ jelet is, mint $\scriptstyle \lnot A\iff _{df}A\rightarrow \bot$.

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.

• Példa: $\scriptstyle A\rightarrow A$ tételséma levezetése

$\scriptstyle (A\rightarrow (B\rightarrow A))$ axiómaséma

$\scriptstyle ((A\rightarrow (B\rightarrow C))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C)))$ axiómaséma

$\scriptstyle ((A\rightarrow (B\rightarrow A))\rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow A)))$ ahol $\scriptstyle C$-t $\scriptstyle A$-ra cseréltük

$\scriptstyle ((A\rightarrow B)\rightarrow (A\rightarrow A))$ modus ponens

$\scriptstyle ((A\rightarrow (B\rightarrow A))\rightarrow (A\rightarrow A))$ ahol $\scriptstyle B$-t $\scriptstyle B\rightarrow A$-ra cseréltük

$\scriptstyle (A\rightarrow A)$ modus ponens

• Példa: $\scriptstyle ((A\lor B)\rightarrow (B\lor A))$ tételséma levezetése

$\scriptstyle (B\rightarrow (B\lor A))$ axiómaséma, ahol $\scriptstyle B$-t $\scriptstyle A$-ra és $\scriptstyle A$-t $\scriptstyle B$-re cseréljük.

$\scriptstyle (A\rightarrow (B\lor A))$ axiómaséma ugyanígy

$\scriptstyle ((A\rightarrow C)\rightarrow ((B\rightarrow C)\rightarrow ((A\lor B)\rightarrow C)))$ axiómaséma

$\scriptstyle ((A\rightarrow (B\lor A))\rightarrow ((B\rightarrow (B\lor A))\rightarrow ((A\lor B)\rightarrow (B\lor A))))$ ahol $\scriptstyle C$-t $\scriptstyle (B\lor A)$-re cseréljük.

$\scriptstyle ((B\rightarrow (B\lor A))\rightarrow ((A\lor B)\rightarrow (B\lor A)))$ modus ponens

$\scriptstyle ((A\lor B)\rightarrow (B\lor A))$ modus ponens

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

Természetes levezetés Logikai konstans Bevezetési szabályok Eltörlési szabályok Nulladrend $\scriptstyle {\bot }$ $\scriptstyle {\frac {A,\lnot A}{\bot }}$ $\scriptstyle {\frac {\bot }{A}}$ $\scriptstyle {\lnot }$ $\scriptstyle {\frac {\begin{array}{c}\scriptstyle [A]\\\scriptstyle \bot \end{array}}{\lnot A}}$ $\scriptstyle {\frac {A,\lnot A}{\bot }}$ $\scriptstyle {\land }$ $\scriptstyle {\frac {A,B}{A\land B}}$ $\scriptstyle {\frac {A\land B}{A}}$ $\scriptstyle {\frac {A\land B}{B}}$ $\scriptstyle {\lor }$ $\scriptstyle {\frac {A}{A\lor B}}$ $\scriptstyle {\frac {A\lor B,{\begin{array}{c}\scriptstyle [A]\\\scriptstyle C\end{array}},{\begin{array}{c}\scriptstyle [B]\\\scriptstyle C\end{array}}}{C}}$ $\scriptstyle {\frac {B}{A\lor B}}$ $\scriptstyle {\rightarrow }$ $\scriptstyle {\frac {\begin{array}{c}\scriptstyle [A]\\\scriptstyle B\end{array}}{A\rightarrow B}}$ $\scriptstyle {\frac {A,A\rightarrow B}{B}}$ Elsőrend $\scriptstyle {\forall }$ $\scriptstyle {\frac {Fa}{\forall xFx}}$ $\scriptstyle {\frac {\forall xFx}{Fa}}$ $\scriptstyle {\exists }$ $\scriptstyle {\frac {Fa}{\exists xFx}}$ $\scriptstyle {\frac {\exists xFx,{\begin{array}{c}\scriptstyle [Fa]\\\scriptstyle C\end{array}}}{C}}$

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ó.

Minden konstansnak lesznek bevezetési szabályai és eltörlési szabályai. A bevezetési szabályok azt jellemzik, hogy milyen premisszákból következtethetünk az adott logikai konstans által összefűzött formulára, míg az eltörlési szabályok azt jellemzik, hogy az adott logikai konstans által összefűzött formulából hogyan lehet következtetni.

A szabályokban $\scriptstyle [A]$-val jelöltük azt, amikor $\scriptstyle A$ nem mint levezetéssel rendelkező formula, hanem csak mint egy feltevés áll rendelkezésünkre. A

$\scriptstyle {\begin{array}{c}\scriptstyle [A]\\\scriptstyle C\end{array}}$

jelölés azt jelenti, hogy $\scriptstyle A$ levezetésével ha rendelkeznénk, akkor $\scriptstyle C$-t le tudnánk vezetni.

Így $\scriptstyle A\lor B$ törlési szabálya például azt jelenti, hogy ha van egy diszjunktív formulánk, intuitíve egy esetszétválasztásunk, melynek mindkét tagjából levezethető lenne egy formula, akkor diszjunktív állításból ilyen módon, de csakis ezzel a feltétellel levezethetjük ezt a formulát.

Ugyanígy, a $\scriptstyle \exists$ eltörlési szabálya azt mondja, hogy ha tudjuk, hogy $\scriptstyle \exists xFx$, akkor amennyiben egy bizonyos $\scriptstyle a$-val $\scriptstyle Fa$-t feltéve levezethető lenne $\scriptstyle C$, akkor ez esetben de csakis ez esetben levezettük $\scriptstyle C$-t.

Ez utóbbi szabály jellemzően intuicionista szabály: A klasszikus logika néhány különös tétele, például a jólrendezési tétel annak köszönhető, hogy úgy is lehet egzisztenciális kvantoros állításra és állításból következtetni, hogy nem áll rendelkezésünkre egy ilyen $\scriptstyle a$, a példa esetében egy ilyen jólrendezés például a valós számok esetében.

A természetes levezetés negációra vonatkozó szabályai az intuicionisták számára is redundánsak. A negációt definiálhatjuk a falsummal a következőképpen: Jelentse $\scriptstyle \lnot A$ azt, hogy $\scriptstyle A$ ellentmondásra vezet, azaz

$\scriptstyle \lnot A\mathop {\iff } _{df}A\rightarrow \bot$.

Ekkor a $\scriptstyle \rightarrow$ bevezetési és eltörlési szabályának (tulajdonképpen a dedukciótételnek és a modus ponensnek) a speciális esetét kapjuk vissza.

• Példa: A disztributivitás egyik iránya: $\scriptstyle ((A\land (B\lor C))\rightarrow ((A\land B)\lor (A\land C))$

$\scriptstyle {\begin{array}{ccc}\scriptstyle [(A\land (B\lor C))]\\\hline \scriptstyle A\\\scriptstyle (B\lor C)&{\begin{array}{c}\scriptstyle [B]\\\hline \scriptstyle (A\land B)\\\hline \scriptstyle ((A\land B)\lor (A\land C))\end{array}}&{\begin{array}{c}\scriptstyle [C]\\\hline \scriptstyle (A\land C)\\\hline \scriptstyle ((A\land B)\lor (A\land C))\end{array}}\\\hline \scriptstyle ((A\land B)\lor (A\land C))\\\hline \scriptstyle ((A\land (B\lor C))\rightarrow ((A\land B)\lor (A\land C)))\end{array}}$

Gentzen típusú szekvenskalkulus

Szekvenskalkulus

Axiómák $\scriptstyle {A\vdash A}$ Strukturális szabályok Premisszák oldalán Konklúzió oldalán $\scriptstyle {\frac {\Gamma \vdash \Theta }{A,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta }{\Gamma \vdash \Theta ,A}}$ $\scriptstyle {\frac {A,A,\Gamma \vdash \Theta }{A,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,A,A}{\Gamma \vdash \Theta ,A}}$ $\scriptstyle {\frac {\Delta ,A,B,\Gamma \vdash \Theta }{\Delta ,B,A,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,A,B,\Lambda }{\Gamma \vdash \Theta ,B,A,\Lambda }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,A\qquad A,\Delta \vdash \Lambda }{\Gamma ,\Delta \vdash \Theta ,\Lambda }}$ Operációs szabályok Bevezetés a premisszákhoz Bevezetés a konklúzióhoz $\scriptstyle {\frac {\Gamma \vdash \Theta ,A}{\lnot A,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {A,\Gamma \vdash \Theta }{\Gamma \vdash \Theta ,\lnot A}}$ $\scriptstyle {\frac {\begin{array}{c}\scriptstyle \Gamma \vdash \Theta ,A\\\scriptstyle \Gamma \vdash \Theta ,B\end{array}}{\Gamma \vdash \Theta ,A\land B}}$ $\scriptstyle {\frac {A,\Gamma \vdash \Theta }{A\land B,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {B,\Gamma \vdash \Theta }{A\land B,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\begin{array}{c}\scriptstyle A,\Gamma \vdash \Theta \\\scriptstyle B,\Gamma \vdash \Theta \end{array}}{A\lor B,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,A}{\Gamma \vdash \Theta ,A\lor B}}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,B}{\Gamma \vdash \Theta ,A\lor B}}$ $\scriptstyle {\frac {\begin{array}{c}\scriptstyle \Gamma \vdash \Theta ,A\\\scriptstyle B,\Delta \vdash \Lambda \end{array}}{A\rightarrow B,\Gamma ,\Delta \vdash \Theta ,\Lambda }}$ $\scriptstyle {\frac {A,\Gamma \vdash \Theta ,B}{\Gamma \vdash \Theta ,A\rightarrow B}}$ $\scriptstyle {\frac {Fa,\Gamma \vdash \Theta }{\forall xFx,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,Fa}{\Gamma \vdash \Theta ,\forall xFx}}$ $\scriptstyle {\frac {Fa,\Gamma \vdash \Theta }{\exists xFx,\Gamma \vdash \Theta }}$ $\scriptstyle {\frac {\Gamma \vdash \Theta ,Fa}{\Gamma \vdash \Theta ,\exists xFx}}$

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$

Ezek a formulasorozatok nem formulahalmazok, ugyanis az elemeinek van egy sorrendjük. Azaz $\scriptstyle A,B,C\vdash A,D$ nem ugyanaz a szekvens, mint$\scriptstyle A,C,B\vdash A,D$.

Fontos továbbá, hogy a Frege-Hilbert-kalkulusnál megszokottaktól eltérően a következő jelsorozatok is értelmes szekvensek:

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

Hogy mégis mindegy a következtetések során az elemek sorrendje, azért már a szekvenskalkulus strukturális szabályai lesznek a felelősek.

A szekvenskalkulusban az axiómák nem formulák, hanem szekvensek, és a levezetési szabályok nem formulákat alakítanak, hanem szekvenseket.

A szekvenskalkulus felépítése:

• Axiómák: A szekvenskalkulusban egyetlen axiómaséma (ami most egy szekvensséma) van, ez pedig $\scriptstyle A\vdash A$.
• Strukturális szabályok: Ide tartoznak azok a szabályok, amelyek a szekvensek struktúráját jellemzik; azt, hogy nem számít a formulák sorrendje, multiplicitása, továbbá a következtetések szempontjából nem számít a premisszák erősítése és a konklúzió gyengítése. Ide tartozik a metszetszabály is, amely az egyetlen olyan szabály lesz, amely által lényegesen is fogyhatnak a szekvensek. A metszetszabály az egyetlen, ami által kifejezések tűnhetnek el úgy, hogy nem maradnak utánuk más kifejezések. Ennek a szabálynak kruciális szerepe lesz a szekvenskalkulus konzisztenciájának bizonyításában.
• Operációs szabályok: A szekvenskalkulus szabályai annyiban nagyon hasonlítanak a természetes levezetésre, hogy ahhoz hasonlóan direkten írja le a logikai konstansok viselkedését. Különbözik azonban itt abban, hogy nem a bevezetésük és eltörlésük szempontjából vizsgálja ezeket, hanem a jobb oldali bevezetésük és bal oldali bevezetésük szempontjából. Teheti ezt azért, mert a szekvenskalkulusnak – mivel szekvensekkel dolgozik–, a levezetésjel mindkét oldala pontosan ugyanúgy a rendelkezésére áll.

Dualitás

A következő levezetéseket érdemes visszafele olvasni. A szekvenskalkulusban ugyanis a természetes levezetéshez hasonlóan könnyen visszafejthető a levezetés a formula alakjának ismeretében.

• Példa: A $\scriptstyle {\frac {\Gamma \vdash \lnot \lnot A,\Theta }{\Gamma \vdash A,\Theta }}$ szekvenslevezetési szabály:

$\scriptstyle \Gamma \vdash \lnot \lnot A,\Theta$ feltevés

$\scriptstyle \lnot A\vdash \lnot A$ axióma

$\scriptstyle \lnot \lnot A,\lnot A\vdash$ negáció bevezetése balra

$\scriptstyle \Gamma ,\lnot A\vdash \Theta$ metszetszabály

$\scriptstyle A\vdash A$ axióma

$\scriptstyle \vdash \lnot A,A$ Negáció bevezetése jobbra

$\scriptstyle \Gamma \vdash A,\Theta$ metszetszabály

• Példa: A $\scriptstyle {\frac {\Gamma ,\lnot \lnot A\vdash \Theta }{\Gamma ,A\vdash \Theta }}$ szekvenslevezetési szabály:

$\scriptstyle \Gamma ,\lnot \lnot A\vdash \Theta$ feltevés

$\scriptstyle \lnot A\vdash \lnot A$ axióma

$\scriptstyle \vdash \lnot \lnot A,\lnot A$ negáció bevezetése jobbra

$\scriptstyle \Gamma \vdash \lnot A,\Theta$ metszetszabály

$\scriptstyle A\vdash A$ axióma

$\scriptstyle \lnot A,A\vdash$ Negáció bevezetése balra

$\scriptstyle \Gamma ,A\vdash \Theta$ metszetszabály

Általában is elmondható egyébként, hogy érvényes egyfajta dualitási tétel a szekvenskalkulusban: Ha egy olyan levezetésben, amelyben nincsen $\scriptstyle \vdash$ jel, tükrözünk minden szekvenst a $\scriptstyle \vdash$ jelre, és az így kapott szekvensben minden logikai jelet kicserélünk a szokásos értelemben vett duálisára, akkor az így kapott kapott szekvenssorozat is egy érvényes szekvenskalkulusbeli levezetés. ($\scriptstyle \land$ és $\scriptstyle \lor$ illetve $\scriptstyle \forall$ és $\scriptstyle \exists$ egymás duálisai.)

Intuicionista és klasszikus szekvenskalkulus

Először álljon itt két példa két jellegzetes formulának levezetésére:

• Példa: A kontrapozíció törvényének intuicionista értelemben is érvényes iránya:

$\scriptstyle A\vdash A$ axióma

$\scriptstyle B\vdash B$ axióma

$\scriptstyle (A\rightarrow B),A\vdash B$ kondicionális bevezetése balra (modus ponens)

$\scriptstyle (A\rightarrow B),\lnot B,A\vdash$ negáció bevezetése balra

$\scriptstyle (A\rightarrow B),\lnot B\vdash \lnot A$ negáció bevezetése jobbra

$\scriptstyle (A\rightarrow B)\vdash (\lnot B\rightarrow \lnot A)$ kondicionális bevezetése jobbra (dedukció-szabály)

$\scriptstyle \vdash (A\rightarrow B)\rightarrow (\lnot B\rightarrow \lnot A))$ kondicionális bevezetése jobbra (dedukció-szabály)

• Példa: A kontrapozíció törvényének csak klasszikus értelemben érvényes iránya:

$\scriptstyle \lnot A\vdash \lnot A$ axióma

$\scriptstyle \lnot B\vdash \lnot B$ axióma

$\scriptstyle (\lnot A\rightarrow \lnot B),\lnot A\vdash \lnot B$ kondicionális bevezetése balra (modus ponens)

$\scriptstyle (\lnot A\rightarrow \lnot B),\lnot A,\lnot \lnot B\vdash$ Negáció bevezetése balra

$\scriptstyle (\lnot A\rightarrow \lnot B),\lnot \lnot B\vdash \lnot \lnot A$ Negáció bevezetése jobbra

$\scriptstyle (\lnot A\rightarrow \lnot B),\lnot \lnot B\vdash A$ Kettős negáció eltüntetése jobboldalt (lásd az első példát)

$\scriptstyle (\lnot A\rightarrow \lnot B),B\vdash A$ Kettős negáció eltüntetése baloldalt (lásd a második példát)

$\scriptstyle (\lnot A\rightarrow \lnot B)\vdash (B\rightarrow A)$ kondicionális bevezetése jobbra (dedukció-szabály)

$\scriptstyle \vdash ((\lnot A\rightarrow \lnot B)\rightarrow (B\rightarrow A))$ kondicionális bevezetése jobbra (dedukció-szabály)

A klasszikus és intuicionista szekvenskalkulus közt annyi a különbség, hogy az intuicionista szekvenskalkulusban a szekvens jobb oldalán mindig legfeljebb csak egyetlen formula lehet. Az utóbbi példában használtuk azt a fentebb bizonyított szabályt, amely eltünteti a kettős negációt. Ennek bizonyításában a szekvensek jobb oldalán előfordul, hogy egynél több formula is van. Eszerint ez a levezetés nem intuicionista. És valóban, ez az a formula, amely karakterizálja a klasszikus Frege-Hilbert kalkulust is (annak harmadik axiómája).

Konzisztencia

A konzisztencia kapcsán érdemes megvizsgálni, hogy hogyan is működik itt az inkonzisztencia. Definíció ugyanaz, mint a szokásos axiómarendszereknél: inkonzisztens a szekvenskalkulus, ha benne minden szekvens levezethető. Be lehet látni, hogy pontosan akkor inkonzisztens a szekvenskalkulus, ha

• levezethető a $\scriptstyle \vdash A\land \lnot A$ ami pontosan akkor igaz, ha
• levezethető az üres szekvens, azaz $\scriptstyle \vdash$.

Könnyű látni, hogy az üres szekvensből valóban pusztán a strukturális szabályok egymás utáni alkalmazásával tetszőleges szekvens előállítható.

A kérdés tehát a következő: Hogyan állíthatjuk elő az üres szekvenst?

A fentiekben volt szó arról, hogy a szekvens kalkulus operációs szabályai nagyon hasonlítanak a természetes levezetésre. Az egyetlen különbség az, hogy mivel ez szekvensekkel dolgozik, eltörlő szabályok helyett alkalmazhat bal oldali bevezetőszabályokat. Ennek az eleganciának nagyon komoly elméleti következménye van. Ha szemügyre vesszük a szekvenskalkulus összes operációs szabályát, a következőt láthatjuk: Mindegyik szabály alkalmazása során a formulák száma nem csökken. Ha tehát pusztán ezeket használnánk, nem lehetne előállítani az üres szekvenst, mivel abban 0 db formula van, míg az egyetlen axiómánkban 2 db, és ennek száma az operatív szabályok alkalmazása során csak nőni tud.

Az üres szekvenst tehát csak a strukturális szabályokkal állíthatjuk elő. Mindössze három olyan strukturális szabály van, amely során csökken a formulák száma a szabályok alkalmazása során. A többször szereplő formulákat egyszerűsítő szabály tesz ki ebből 2-t, ami azonban nyilvánvalóan legfeljebb 1 darabig tudja csökkenteni a szekvensben szereplő formulák számát.

Az üres szekvenst tehát csak a metszetszabállyal, az utolsó strukturális szabállyal lehet előállítani, nevezetesen ha a szabályban minden formulasorozat üres, amivel egyébként hamar visszakaphatjuk az inkonzisztencia szokásos okozóját, az ellentmondó formulapárt.

Ily módon adódik, hogy a szekvenskalkulus konzisztenciáját a következő, Gentzen és a szakirodalom által csak „Hauptsatz”-nak nevezett tétel biztosítja:

• Tétel (Hauptsatz): Minden szekvenskalkulusban levő levezetéshez létezik olyan levezetés, amelynek ugyanaz az utolsó szekvense, és amelyben nincs felhasználva a metszetszabály.

Ha tehát a szekvenskalkulus inkonzisztens lenne, akkor az üres szekvens tétele lenne. Ha tétele az üres szekvens, akkor van egy olyan szekvenslevezetés, amelynek ez van a végén. A Hauptsatz miatt azonban ekkor kell legyen egy olyan levezetés is, amelynek a végén szintén az üres szekvens van, ugyanakkor amiben nem volt felhasználva a metszetszabály. Ez viszont lehetetlen, mivel a szabályok alkalmazása során a szekvensbeli formulák száma sosem lehet kevesebb 1-nél. Tehát lehetetlen, hogy a szekvenskalkulus inkonzisztens legyen. Ezzel beláttuk, hogy a szekvenskalkulus konzisztens.

Ezzel azonban nem csak a szekvenskalkulus konzisztenciáját bizonyítottuk. Létezik ugyanis egy megfeleltetés a szekvenskalkulusok és pl. a Frege-Hilbert kalkulusok közt:

• Klasszikus logikában: A szekvenskalkulusban levezethető az $\scriptstyle \vdash A$ szekvens akkor és csak akkor, ha egy klasszikus Frege-Hilbert kalkulusban levezethető az $\scriptstyle A$ formula.
• Intuicionista logikában: A szekvenskalkulusban pontosan akkor vezethető le úgy az $\scriptstyle \vdash A$ szekvens, hogy a szekvens jobb oldalán mindig csak egyetlen formula van, ha egy intuicionista Frege-Hilbert kalkulusban levezethető az $\scriptstyle A$ formula.

Források

• Ruzsa Imre. Logikai szintaxis és szemantika I. (magyar nyelven). Budapest: Akadémiai Kiadó (1988). ISBN 963-05-4720-1 
• Alexander Chagrov – Michael Zakharyaschev. Modal Logic. Oxford: Clarendon Press (1997). ISBN 9780198537793 
• Ruzsa, Imre, Máté András. Bevezetés a modern logikába. Budapest: Osiris Kiadó (1997). ISBN 963-379-185-5 
• Pásztorné Varga Katalin - Várterész Magda. A matematikai logika alkalmazásszemléletű tárgyalása. Budapest: Panem Könyvkiadó (2003). ISBN 963-545-364-7 
• 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)