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 formula vagy formulaséma logikai igazság, a következőképpen jelöljük:
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 formulából vagy formulasémából (premisszából) levezethető egy formula vagy formulaséma (konklúzió), a következőképpen jelöljük:
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 véges vagy végtelen formulahalmaz vagy egy formulasorozat, akkor azt, hogy -ból levezethető egy állítás, a következőképpen jelöljük:
Ennek megfelelően az, hogy egy 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 és két ilyen formulasorozat, akkor
intuitíve azt jelenti, hogy -beli formulák konjunkciójából levezethető a -beli formulák diszjunkciója, azaz 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 jelet használni. Általában pedig a azt jelenti, hogy az formula vagy formulaséma megkapható a logikai kalkulus axiómáiból és a 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. és szintaktikailag ekvivalensek, ha és . Ezt néha a következőképpen jelölik:
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 . A -t meghatározó kalkulus helyes a -t meghatározó szemantikára nézve, ha -ból következik .
Ilyen például egy intuicionista kalkulus egy klasszikus szemantikára nézve. A -t meghatározó kalkulus teljes a -t meghatározó szemantikára nézve, ha -ból következik .
Ilyen például egy inkonzisztens kalkulus bármilyen szemantikára nézve. A -t meghatározó kalkulus adekvát a -t meghatározó szemantikára nézve, ha helyes és teljes, azaz ha akkor és csak akkor, ha .
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) (A2) (A3) Levezetési szabályok: (MP) Elsőrend Axiómasémák (A4) (A5) Levezetési szabály: (UG)
A klasszikus logikának sokféle axiomatizálása van, az egyik legelterjedtebb a Łukasiewitztől eredő három axiómás jelekkel dolgozó rendszer.
Az elsőrendű kalkulusnál fontos kitétel, hogy az (UG) szabály alkalmazásakor az -ban -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: levezetési szabály bizonyítása. Eszerint ha rendelkezünk egy alakú tétellel, akkor le tudjuk vezetni az tételt is. Ez a feltevés. az első axiómasémában -t -ra cseréltük, -t pedig -ra. modus ponens (A3) axiómaséma, amiben -t -ra cseréltük, -t pedig -ra. modus ponenes (A3) axiómaséma, amiben -t -ra cseréltük. modus ponens 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) (A2) (A3) (A4) (A5) (A6) (A7) (A8) (A9) Levezetési szabályok: (MP) Elsőrend Axiómasémák (A10) (A11) Levezetési szabályok: (UG) (EG) |} 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 terminus szabad -re nézve. (EG) és univerzális generalizációnál (UG) nem lehet -nek -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 jelet azonban is rövidítésként vezetjük be, továbbá a jelet is, mint .
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: tételséma levezetése axiómaséma axiómaséma ahol -t -ra cseréltük modus ponens ahol -t -ra cseréltük modus ponens Példa: tételséma levezetése axiómaséma, ahol -t -ra és -t -re cseréljük. axiómaséma ugyanígy axiómaséma ahol -t -re cseréljük. modus ponens 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 Elsőrend
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 -val jelöltük azt, amikor nem mint levezetéssel rendelkező formula, hanem csak mint egy feltevés áll rendelkezésünkre. A
jelölés azt jelenti, hogy levezetésével ha rendelkeznénk, akkor -t le tudnánk vezetni.
Így 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 eltörlési szabálya azt mondja, hogy ha tudjuk, hogy , akkor amennyiben egy bizonyos -val -t feltéve levezethető lenne , akkor ez esetben de csakis ez esetben levezettük -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 , a példa esetében egy ilyen jólrendezés például a valós számok esetében.A jólrendezési tétel a valós számokra alkalmazva azzal a következménnyel jár, hogy a valós számoknak lesz valami olyan különös rendezése, mely szerint minden valós számhalmaznak lesz egy minimális eleme; olyan eleme, melynél semmi más eleme nem kisebb. A valós számok szokásos rendezése természetesen nem ilyen, mivel ott például a negatív számok halmaza vagy a nyílt intervallumnak nincsen legkisebb eleme; minden elemnél van kisebb. A tétel egy olyan rendezés létezését állítja, amelynek máig is pusztán a létezése bizonyított.
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 azt, hogy ellentmondásra vezet, azaz . Ekkor a 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:
Gentzen típusú szekvenskalkulus Szekvenskalkulus Axiómák Strukturális szabályok Premisszák oldalán Konklúzió oldalán Operációs szabályok Bevezetés a premisszákhoz Bevezetés a konklúzióhoz
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
alakú jelsorozatokat, ahol és olyan rendezett jelsorozatok, amelyeknek minden tagja egy formula. A bal oldalán lévő formulákat „és”-sel érdemes kiolvasni, a jobb oldalán lévő formulákat pedig „vagy”-gyal. Tehát
kiolvasva: -ból -ből és -ből együtt következik vagy
Ezek a formulasorozatok nem formulahalmazok, ugyanis az elemeinek van egy sorrendjük. Azaz nem ugyanaz a szekvens, mint.