Szekvenskalkulus

A matematikai logikában, a szekvenskalkulus lényegében a formális logikai érvelés egy stílusa, ahol a bizonyítás minden sora feltételes tautológia (Gerhard Gentzen nyomán szekvensnek hívva) feltétel nélküli tautológia helyett. Minden feltételes tautológiát a korábbi sorok egyéb feltételes tautológiáiból következtetünk egy formális argumentumban, a következtetési szabályok és eljárások szerint, ezzel jobb megközelítést adva a matematikusok által használt természetes levezetési stílushoz, mint David Hilbert korábbi stílusú formális logikája, ahol minden sor feltétel nélküli tautológia volt. Előfordulhat, hogy finomabb megkülönböztetéseket kell tenni; például, előfordulhatnak nem logikus axiómák, amelyekre minden ítélet implicit módon függ. Ezután a szekvenciák a feltételes tautológiák helyett a feltételes tételeket jelzik egy elsőrendű nyelvben.

A szekvenskalkulus egyike a bizonyítási kalkulus számos létező stílusának, ami a soronkénti logikai argumentumok kifejezésére szolgál.

Hilbert-stílus. Minden sor feltétel nélküli tautológia (vagy tétel).
Gentzen-stílus. Minden sor feltételes tautológia (vagy tétel), amelynek nulla vagy több feltétele van a bal oldalon.
- Természetes levezetés. Minden (feltételes) sornak pontosan egy állított ítélete van a jobb oldalon.
- Szekvens kalkulus. Minden (feltételes) sornak nulla vagy több állított ítélete van a jobb oldalon.

Más szóval, a természetes levezetés és a szekvenskalkulus rendszerek a Gentzen-stílusú rendszerek sajátosan eltérő fajtái. A Hilbert-stílusú rendszereknek általában nagyon kevés számú következtetési szabályuk van, jobban támaszkodnak az axiómák halmazára. A Gentzen-stílusú rendszereknek általában nagyon kevés axiómájuk van, ha vannak ilyenek, inkább a szabályrendszerekre támaszkodnak.

A Gentzen-stílusú rendszerek jelentős gyakorlati és elméleti előnyökkel rendelkeznek a Hilbert-stílusú rendszerekhez képest. Például mind a természetes levezetés, mind a szekvens kalkulusrendszerek megkönnyítik az egyetemes és egzisztenciális kvantorok eliminációját és bevezetését annak érdekében, hogy a nem definiált logikai kifejezések manipulálhatók legyenek az Ítéletlogika sokkal egyszerűbb szabályai szerint. Egy tipikus argumentumban a kvantorok megszűnnek, majd az ítéletlogikát alkalmazzák a nem definiált kifejezésekre (amelyek általában szabad változókat tartalmaznak), majd a kvantorok újra bevezetésre kerülnek. Ez nagyon hasonlít a matematikai bizonyítások gyakorlatban történő végrehajtásának módjára a matematikusok szerint. A predikátum kalkulus bizonyításait általában sokkal könnyebb felfedezni ezzel a megközelítéssel, és gyakran még rövidebbek is. A természetes levezetéses rendszerek jobban megfelelnek a gyakorlati tétel-bizonyításnak. A Szekvens kalkulus rendszerek jobban megfelelnek az elméleti elemzésnek.

Áttekintés

A bizonyításelméletben és a matematikai logikában a szekvenskalkulus a logikai kalkulus családja, amelyek megosztanak egy bizonyos következtetési stílust és bizonyos formai tulajdonságokat. Az első szekvenskalkulus rendszereket, az LK-t és az LJ-t 1934-1935-ben Gerhard Gentzen^[1] vezette be a természetes levezetés, elsőrendű logikában történő tanulmányozásának eszközeként (klasszikus és intuíciós verziókban). Gentzen LK-ról és LJ-ről szóló úgynevezett "fő tétele" (Hauptsatz) a Cut-eliminációs tétel volt,^[2]^[3] amelynek eredménye messzemenő meta-elméleti következményekkel járt, ideértve a következetességet is . Gentzen néhány évvel később tovább demonstrálta ennek a technikának a hatékonyságát és rugalmasságát, egy Cut-eliminációs argumentum alkalmazásával (transzfinit) bizonyítékként szolgál a Peano aritmetika konzisztenciájáról, meglepő válaszként Gödel nemteljességi tételeire. Azokból az időkből kiindulva, a szekvenskalkulust, más néven Gentzen-rendszereket,^[4]^[5]^[6]^[7] és a hozzájuk kapcsolódó általános fogalmakat széles körben alkalmazzák a bizonyításelmélet, a matematikai logika és az automatizált levezetés területén .

Hilbert-stílusú levezetéses rendszerek

A levezetéses rendszerek különböző stílusainak osztályozásának egyik módja az, ha megnézzük a rendszerben az ítéletek formáját, vagyis hogy mely dolgok jelenhetnek meg egy (al) bizonyítás következtetéseként. A legegyszerűbb ítéletformát a Hilbert-stílusú levezetéses rendszerekben használják, ahol az ítéletnek van formája

B

Ahol $B$ az elsőrendű logika bármely formulája (vagy bármilyen logikára is alkalmazható a levezetéses rendszer, pl . ítéletlogikára, magasabb rendű logikára vagy modális logikára). A tételek azok a formulák, amelyek érvényes bizonyítékként záró ítéletként jelennek meg. A Hilbert-stílusú rendszer nem igényel megkülönböztetést a formulák és az ítéletek között; itt csak egyet készítünk, kizárólag a következő esetekkel való összehasonlítás céljából.

A Hilbert-stílusú rendszer egyszerű szintaxisáért fizetett ár az, hogy a teljes formális bizonyítások általában rendkívül hosszúak. Egy ilyen rendszerben a bizonyításokkal kapcsolatos konkrét argumentumok szinte mindig a levezetéses tételre hivatkoznak . Ez ahhoz az ötlethez vezet, hogy a levezetéstételt formális szabályként illesszék be a rendszerbe, ami a természetes levezetésben történik.

Természetes levezetéses rendszerek

A természetes levezetésben az ítéleteknek van formája

A_{1},A_{2},\ldots ,A_{n}\vdash B

ahol az $A_{i}$ és $B$ formulák és $n\geq 0$ . Az $A_{i}$ permutációi nem lényegesek. Más szavakkal, egy ítélet egy formulából (esetleg üres formulából) áll a " $\vdash$ " szimbólum (forgókereszt szimbólum) bal oldalán, és egyetlen formulából a jobb oldalon.^[8]^[9]^[10] A tételek azok a $B$ formulák, oly módon, hogy $\vdash B$ (üres bal oldallal) egy érvényes bizonyítás következtetése. (A természetes levezetés egyes bemutatásaiban az $A_{i}$ -k a forgókeresztet nem írják fel kifejezetten; ehelyett kétdimenziós jelölést használnak, amelyből következtetni lehet. )

A természetes levezetésben alkalmazott ítélet szokásos szemantikája az, hogy azt állítja, hogy bármikor^[11] $A_{1}$ , $A_{2}$ stb., mind igazak, akkor $B$ is igaz lesz. Az ítéletek

A_{1},\ldots ,A_{n}\vdash B

és

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow B

egyenértékűek abban az erős értelemben, hogy bármelyik igazolása kiterjeszthető a másik igazolására is.

Szekvenskalkulus rendszerek

Végül a szekvenskalkulus általánosítja a természetes levezetéses ítélet formáját

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

egy szekvenciának nevezett szintaktikai objektumra. A forgókereszt szimbólum bal oldalán található formulákat előzménynek, a jobb oldali formulákat pedig következményeknek nevezzük; együttesen szekvenseknek nevezzük őket.^[12] Újra: $A_{i}$ és $B_{i}$ fromulák, $n$ és $k$ nem negatív egész számok, vagyis a bal vagy a jobb oldal (vagy egyik sem vagy mindkettő) üres lehet. A természetes levezetéshez hasonlóan a tételek azok a $B$ -k is, ahol $\vdash B$ egy érvényes bizonyíték következtetése.

Egy szekvens alapértelmezett szemantikája egy állítás, hogy amikor minden $A_{i}$ igaz, legalább egy $B_{i}$ is igaz lesz.^[13] Így az üres sorozat, amelynek mindkét szekvense üres, hamis.^[14] Ennek egyik módja az, hogy a forgókereszt szimbólum bal oldalán lévő vesszőt "és" -ként kell gondolni, a forgókereszttől jobbra lévő vesszőt pedig (befogadó) "vagy" kifejezésre kell gondolni. A szekvensek

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}

és

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})

egyenértékűek abban az erős értelemben, hogy bármelyik igazolása kiterjeszthető a másik igazolására is.

Első látásra az ítéletforma ilyen kiterjesztése furcsa bonyodalomnak tűnhet – ezt nem a természetes levezetés nyilvánvaló hiányosságai indokolják meg, és kezdetben zavaró, hogy a vessző a forgókereszt jelek két oldalán teljesen más dolgokat jelentenek. Klasszikus kontextusban azonban a szekvens szemantikája (ítéletlogikai tautológia segítségével) kifejezhető akár

\vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}

(legalább az egyik A hamis, vagy az egyik B igaz) vagy

\vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})

(nem fordulhat elő, hogy az összes A igaz és az összes B hamis). Ezekben a megfogalmazásokban az egyetlen különbség a forgókereszt két oldalán lévő formulák között az, hogy az egyik oldal tagadás. Így a bal oldalt a jobbra cserélni egy szekvensben az összes alkotó formula tagadásának felel meg. Ez azt jelenti, hogy egy olyan szimmetria, mint De Morgan azonosságai, amely szemantikai szinten logikai tagadásként nyilvánul meg, közvetlenül a szekvensek bal-jobb szimmetriájává válik – és valóban, a konjunkció (∧) kezelésére szolgáló szekvenskalkulus következtetési szabályai a diszjunkcióval foglalkozók tükörképei (∨).

Sok logikus úgy érzi hogy ez a szimmetrikus bemutatás mélyebb betekintést kínál a logika felépítésébe, mint a más bizonyítási rendszer stílusai, ahol a tagadás klasszikus kettőssége nem annyira nyilvánvaló a szabályokban.

Különbség a természetes levezetés és a szekvenskalkulus között

Gentzen éles különbséget tett az egykimenetű természetes levezetéses rendszerei (NK és NJ) és a több kimenetű szekvenskalkulus rendszerei (LK és LJ) között. Azt írta, hogy az intuitív természetes levezetéses rendszer NJ kissé csúnya.^[15] Elmondta, hogy a kizárt középső speciális szerepe a klasszikus természetes levezetéses rendszerben NK megszűnik az LK klasszikus szekvenciális számítási rendszerben.^[16] Azt mondta, hogy a szekvenskalkulus LJ több szimmetriát adott, mint a természetes leveztés NJ az intuíciós logika esetében, akárcsak a klasszikus logika esetében (LK versus NK).^[17] Aztán elmondta, hogy ezen okok mellett a szekvenskalkulus, több szukcessziós képlettel különösen, az ő fő tételéhez ("Hauptsatz") szánják.^[18]

A "szekvens" szó eredete

A "szekvencia" szót a "Sequenz" szóból vettük át Gentzen 1934-es cikkében.^[1] Kleene a következő megjegyzést fűzte az angol nyelvű fordításhoz: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any succession of objects, where the German is 'Folge'."^[19]

Logikai formulák bizonyítása

Redukciós fák

A szekvenskalkulus a formulák ítéletlogikában történő bizonyításának eszközének tekinthető, hasonlóan az analitikus táblák módszeréhez. Lépéssorozatot ad, amely lehetővé teszi, hogy a logikai formulák bizonyításának problémáját egyszerűbb és egyszerűbb formulákká csökkentsék mindaddig, amíg el nem jutnak triviális egyedekhez.^[20]

Vegyük figyelembe a következő formulát:

((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

Ez a következő formában van megírva, ahol a bebizonyítandó javaslat a forgókereszt szimbólumtóljobbra található $\vdash$ :

\vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

Most ahelyett, hogy ezt az axiómák alapján bizonyítanánk, elegendő feltételezni a implikáció premisszáját, majd megpróbálni bizonyítani annak konklúzióját.^[21] Ezért az egyik a következő szekvensre lép:

(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r

A jobb oldal megint tartalmaz egy implikációt, amelynek premisszája tovább feltételezhető, így csak annak konklúzióját kell bizonyítani:

(p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r

Mivel feltételezzük, hogy a bal oldali argumentumok konjugálnak, ezek helyettesíthetők a következőkkel:

(p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r

Ez ekvivalens a baloldal első argumentumának mindkét esetben történő disszjunktív konklúziók bizonyításával. Így ketté oszthatjuk a szekvenst, ahol most mindegyiket külön kell igazolnunk:

p\rightarrow r,p,q\vdash r

q\rightarrow r,p,q\vdash r

Az első ítélet esetében átírjuk $p\rightarrow r$ -t mint $\lnot p\lor r$ -re és ismét szétválasztjuk a szekvenst, hogy:

\lnot p,p,q\vdash r

r,p,q\vdash r

A második szekvens elkészült; az első szekvens tovább egyszerűsíthető:

p,q\vdash p,r

Ez a folyamat mindaddig folytatható, amíg mindkét oldalon csak atomi formulák maradnak. A folyamat grafikusan leírható egy gyökeres fa gráffal, ahogy a jobb oldalon látható. A fa gyöke az a formula, amelyet be akarunk bizonyítani; a levelek csak atomi formulákból állnak. A fa redukciós faként ismert.^[20]^[22]

A forgókereszttől balra lévő elemeket konjunkcióval, a jobb oldali elemeket pedig diszjunkcióval kötjük össze. Ezért, ha mindkettő csak atomi szimbólumokból áll, a szekvens akkor és csak akkor fogadható el axiomatizálhatóan (és mindig igazként), ha a jobb oldalon lévő szimbólumok közül legalább az egyik a bal oldalon is megjelenik.

Kövessük azokat a szabályokat, amelyek a fán haladnak tovább. Valahányszor egy szekvenst kettéválasztunk, a facsúcsnak két gyermekcsúcsa lesz, és a fa elágazik. Ezenkívül szabadon megváltoztathatja az argumentumok sorrendjét mindkét oldalon; Γ és Δ jelölik a lehetséges további argumentumokat.^[20]

A Gentzen-stílusú elrendezésekben a természetes levezetéshez használt vízszintes vonal szokásos kifejezése a következtetési vonal.^[23]

Bal:	Jobb:
$L\land$ szabály: $\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}$	$R\land$ szabály: ${\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}$
$L\lor$ szabály: ${\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}$	$R\lor$ szabály: $\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}$
$L\rightarrow$ szabály: ${\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}$	$R\rightarrow$ szabály: $\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}$
$L\lnot$ szabály: $\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}$	$R\lnot$ szabály: $\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}$
Axióma:
$p,r\vdash q,r$

Az ítéletlogika bármelyik formulájával kezdve, lépések sorozatával a forgókereszt jobb oldala addig dolgozható fel, amíg csak atomi szimbólumokat tartalmaz. Ezután ugyanez történik a bal oldalon is. Mivel minden logikai operátor megjelenik a fenti szabályok egyikében, és a szabály eltávolítja őket, a folyamat akkor fejeződik be, ha nem maradnak logikai operátorok: A formula lebomlott.

Így a fák leveleinek szekvensei csak atomi szimbólumokat tartalmaznak, amelyeket vagy az axióma bizonyíthat, vagy sem, aszerint, hogy a jobb oldalon látható szimbólumok egyike is megjelenik-e a bal oldalon.

Könnyen belátható, hogy a fa lépései megőrzik az általuk implikált formulák szemantikai igazságértékét, és a fa különböző ágai között konjunkcióval értendő, amikor hasadás történik. Az is nyilvánvaló, hogy egy axióma akkor és csak akkor bizonyítható, ha igaz az igazságértékek minden hozzárendeléséhez, az atomi szimbólumokhoz. Így ez a rendszer megbízható és teljes a klasszikus ítéletlogika szempontjából.

Kapcsolat a standard axiomatizációkkal

A szekvenskalkulus összefügg az ítéletlogika egyéb axiomatizációival, például Frege ítéletlogikájával vagy Jan Łukasiewicz axiomatizálásával (maga a standard Hilbert-rendszer része ): Minden ezekben bizonyítható formulának van redukciós fája.

Ez a következőképpen mutatható ki: Az ítéletlogika minden bizonyítéka csak axiómákat és következtetési szabályokat használ. Az axióma sémájának minden egyes használata igaz logikai formulát eredményez, és így szekvenskalkulussal igazolható. A fent említett rendszerek egyetlen következtetési szabálya a modus ponens, amelyet a Cut szabály által implementálunk.

Az LK rendszer

Ez a szakasz bemutatja az LK szekvenskalkulus szabályait, amelyeket Gentzen vezetett be 1934-ben. (LK, unintuitively, a „K lassische Prädikaten l ogik”.) ^[24] A (formális) bizonyíték ebben a kalkulusban a szekvensek szekvenciája, ahol mindegyik szekvens levezethető a szekvensekben korábban megjelenő szekvenciákból az alábbi szabályok egyikének alkalmazásával.

Következtetési szabályok

A következő jelölést kell használni:

$\vdash$ jel a forgókeresztként ismert, elválasztja a bal oldali feltételezéseket a jobb oldali ítéletektől.
$A$ és $B$ jelölje az elsőrendű predikátum logika formuláit (ezt korlátozhatjuk az ítéletlogikára is),
$\Gamma ,\Delta ,\Sigma$ $\Gamma ,\Delta ,\Sigma$ , és $\Pi$ $\Pi$ a formulák véges (esetleg üres) szekvenciái (valójában a formulák sorrendje nem számít), amelyeket kontextusoknak nevezünk,
- A $\vdash$ bal oldalán a formulasorozatot konjunktívnak tekintjük (feltételezzük, hogy mind egyszerre tartanak),
- míg a $\vdash$ jobb oldalán a formulasorozat diszjunktívnak tekintendő (a változók hozzárendeléséhez legalább a formulák egyikének meg kell felelnie),
$t$ tetszőleges kifejezést jelöl,
$x$ és $y$ jelölje a változókat.
egy változó szabadon fordul elő egy formulán belül, ha a $\forall$ vagy $\exists$ kvantorok hatókörén kívül esnek.
$A[t/x]$ a formulát jelöli, amelyet a $t$ kifejezés helyettesítésével kapunk az $x$ változó minden szabad előfordulásához az $A$ formulában azzal a megkötéssel, hogy a $t$ kifejezésnek szabadnak kell lennie az $x$ változó számára $A$ -ban (azaz egyetlen változó sem fordul elő a $t$ -ben, ami így bekötődik $A[t/x]$ -be).
$WL$ , $WR$ , $CL$ , $CR$ , $PL$ , $PR$ : Ez a hat szerkezeti szabály a három szerkezeti szabály két változatának felel meg; az egyik a $\vdash$ bal oldalán („L”) használható, és a másik a jobb oldalán („R”). A szabályok rövidítése: „W” a gyengüléshez (bal / jobb), „C” a kontrakcióhoz és „P” rövidítés a permutációhoz .

Vegyük figyelembe, hogy a fent bemutatott redukciós fa mentén történő haladás szabályaival ellentétben a következő szabályok az ellentétes irányú haladásra vonatkoznak, az axiómáktól a tételekig. Így ezek pontos tükörképei a fenti szabályoknak, azzal a különbséggel, hogy itt a szimmetriát nem implicit módon feltételezzük, és kvantorra vonatkozó szabályokat adunk hozzá.

Axióma:	Vágott:
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
Bal logikai szabályok:	Jobb logikai szabályok:
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
Bal szerkezeti szabályok:	Jobb szerkezeti szabályok:
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

Korlátozások: Az $({\forall }R)$ és $({\exists }L)$ szabályokban az $y$ változó sehol sem fordulhat elő szabadon a megfelelő alsó szekvenciákban.

Intuitív magyarázat

A fenti szabályok két nagy csoportra oszthatók: logikai és strukturális szabályokra . A logikai szabályok mindegyike új logikai formulát vezet be a $\vdash$ forgókereszt bal vagy jobb oldalán . Ezzel szemben a szerkezeti szabályok a szekvensek szerkezetén működnek, figyelmen kívül hagyva a formulák pontos alakját. Az általános séma két kivétele az identitás axióma (I) és a Cut szabálya.

Habár formálisan is kimondják, a fenti szabályok a intuitív olvasást teszik lehetővé a klasszikus logika szempontjából. Vegyük például a $({\land }L_{1})$ szabályt . Azt mondja, hogy valahányszor a $\Delta$ -t bizonyítani lehet, $A$ tartalmazhat valamilyen formulaszekvenciát, akkor következtetni is lehet $\Delta$ -ra abból a (erősebb) feltételezésből, amit $A\land B$ tart. Hasonlóképpen a $({\neg }R)$ szabály kijelenti, hogy ha $\Gamma$ és $A$ elég a $\Delta$ következtetéséhez, aztán $\Gamma$ -t egyedül lehet még következtetni, akkor $\Delta$ -nak vagy $A$ -nak hamisnak kell lennie, azaz ${\neg }A$ tart. Az összes szabály így interpretálható.. A kvantorszabályokkal kapcsolatos intuícióért vegyük figyelembe az $({\forall }R)$ szabályt. Természetesen az $\forall {x}A$ csak abból a tényből áll, hogy igaz értékű $A[y/x]$ általában nem lehetséges. Ha azonban az y változót máshol nem említik (azaz továbbra is szabadon választható, a többi formula befolyásolása nélkül), akkor feltételezhetjük, hogy $A[y/x]$ bármely értékére érvényes az y. A többi szabálynak innentől kezdve egyértelműnek kell lennie.

Ahelyett, hogy a szabályokat a predikátumlogikában szereplő legális derivációk leírásaként tekintenénk, tekinthetjük őket utasításként egy adott állítás igazolásának elkészítéséhez is. Ebben az esetben a szabályok alulról-felfelé olvashatók; például, $({\land }R)$ azt írja le, hogy $A\land B$ a $\Gamma$ és $\Sigma$ feltételezésekből következik, elegendő azt bizonyítani, hogy $A$ a $\Gamma$ -ból következtet, illetőleg $B$ a $\Sigma$ -ból következtet. Vegyük figyelembe, hogy bizonyos előzmények ismeretében nem világos hogyan kell $\Gamma$ -t és $\Sigma$ -t felosztani. Azonban csak véglegesen sok lehetőség ellenőrizhető, mivel a feltételezés előzménye véges. Ez azt is szemlélteti, hogy a bizonyítási elmélet kombinatorikus módon miként működik a bizonyításokon: $A$ -ra és $B$ -re is adott bizonyítást, lehet építeni $A\land B$ -re egy bizonyítást.

Ha valamilyen bizonyítást keres, a legtöbb szabály többé-kevésbé közvetlen eljárásokat kínál arra, hogyan kell ezt megtenni. A cut szabálya más: kimondja, hogy amikor egy $A$ formulára következtetni lehet, és ez a formula szolgálhat előfeltételként más állítások megkötésére is, akkor az $A$ formula "kivágható" és a megfelelő derivációk összekapcsolódnak. Bizonyos alulról felfelé építkezéskor ez az $A$ találgatásának problémáját idézi elő (mivel az alábbiakban egyáltalán nem jelenik meg). A cut-eliminációs tétel tehát döntő fontosságú a szekvenskalkulus automatizált levezetésben való alkalmazásában: azt állítja, hogy a Cut szabály minden felhasználása eliminálható egy bizonyításból, ami azt jelenti, hogy bármely bizonyítható szekvens cut-free bizonyítást kaphat.

A második, kissé különleges szabály az identitás axióma (I). Ennek intuitív olvasata nyilvánvaló: minden formula bizonyítja önmagát. A Cut szabályhoz hasonlóan az identitás axióma is némileg redundás: az atomi kezdeti szekvenciák teljessége kijelenti, hogy a szabály az atomi formuláka korlátozható a bizonyíthatóság elvesztése nélkül.

Vegyük észre, hogy minden szabálynak van társa, kivéve a következtetésre vonatkozó szabályoknak. Ez azt a tényt tükrözi, hogy az elsőrendű logika szokásos nyelve nem tartalmazza a "nem implikált" kötőszót $\not \leftarrow$ ez lenne a De Morgan kettős implikáció. Ha ilyen összekötőt adunk a természetes szabályaihoz, akkor a számítás teljesen bal-jobb szimmetrikus lesz.

Példa derivációk

Itt van a " $\vdash A\lor \lnot A$ " levezetése, amelyet a kizárt harmadik elve (latinul tertium non datur) törvényeként ismerünk.

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(\lor R_{2})$
$\vdash A\lor \lnot A,A$
		$(PR)$
$\vdash A,A\lor \lnot A$
		$(\lor R_{1})$
$\vdash A\lor \lnot A,A\lor \lnot A$
		$(CR)$
$\vdash A\lor \lnot A$

Következő a kvantorokkal kapcsolatos egyszerű tényező bizonyítása. Ne feledjük, hogy ez fordítva nem igaz, és valótlansága akkor látható, amikor megpróbáljuk alulról felfelé levezetni, mert egy meglévő szabad változó nem használható fel a $(\forall R)$ és $(\exists L)$ szabályok helyettesítésére.

		$(I)$
$p(x,y)\vdash p(x,y)$
		$(\forall L)$
$\forall x\left(p(x,y)\right)\vdash p(x,y)$
		$(\exists R)$
$\forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\exists L)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\forall R)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)$

Bebizonyítjuk, hogy: ${\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$ .Könnyű megtalálni a levezetést, amely szemlélteti az LK hasznosságát az automatizált bizonyításban.

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(PR)$
$\vdash A,\lnot A$

			$(I)$
$B\vdash B$			$(I)$
$B\vdash B$

			$(I)$
$C\vdash C$			$(I)$
$C\vdash C$

(\lor L)

B\lor C\vdash B,C

(PR)

B\lor C\vdash C,B

(\lnot L)

B\lor C,\lnot C\vdash B

		$(I)$
$\lnot A\vdash \lnot A$		$(I)$
$\lnot A\vdash \lnot A$

(\rightarrow L)

\left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A

(\land L_{1})

\left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A

(\land L_{2})

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(CL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A

(\rightarrow L)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A

(CR)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A

(PL)

\left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(\rightarrow R)

\left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)

(\rightarrow R)

\vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)

Ezek a deriválások a szekvenskalkulus szigorúan formális felépítését is hangsúlyozzák. Például a fent definiált logikai szabályok mindig a forgókereszt közvetlenül szomszédos formuláján hatnak, így a permutációs szabályok szükségesek. Ne feledjük azonban, hogy ez részben a bemutatás tárgya, eredeti Gentzen stílusban. A gyakori szimplifikáció magában foglalja a formulák multihalmazának használatát, szekvencia helyett a szekvensek értelmezésében, eliminálva egy kifejezett permutációs szabály szükségességét. Ez megfelel a feltételezések és a derivációk kommutativitásának eltolódásának a szekvenskalkuluson kívül, míg az LK beágyazza magát a rendszerbe.

Reláció az analitikus táblákkal

A szekvenskalkulus bizonyos megfogalmazásai (azaz variánsai) esetében az ilyen számításban szereplő bizonyítás izomorf az egy fejjel lefelé zárt analitikus táblához képest.^[25]

Strukturális szabályok

A strukturális szabályok további vitát érdemelnek.

A gyengülés (W) lehetővé teszi tetszőleges elemek hozzáadását egy sorozathoz. Intuitív módon, ez az előzményben megengedett, mert mindig korlátozhatjuk a bizonyításunk körét (ha minden autónak van kereke, akkor nyugodtan mondhatjuk, hogy minden fekete autónak van kereke); és a folytatásban is, mert mindig megengedhetjük az alternatív következtetéseket (ha minden autónak van kereke, akkor nyugodtan mondhatjuk, hogy minden autónak van kereke vagy szárnya).

A kontrakció (C) és a permutáció (P) biztosítja, hogy sem a szekvenciák elemeinek sorrendje (P), sem az előfordulások sokasága (C) nem számít. Így a szekvenciák helyett a halmazokat is figyelembe lehet venni.

A szekvenciák alkalmazásának további erőfeszítése azonban indokolt, mivel a strukturális szabályok egy része vagy egésze kihagyható. Ezzel megszerezzük az úgynevezett szubstrukturális logikákat .

Az LK rendszer tulajdonságai

Ez a szabályrendszer megalapozottnak és teljesnek mutatható ki az elsőrendű logika, azaz $A$ utasítás szempontjából szemantikailag következik $\Gamma$ $(\Gamma \vDash A)$ premisszájából csak akkor, ha a $\Gamma \vdash A$ szekvens a fenti szabályok alapján levezethető.^[26]

A szekvenskalkulusban a Cut-elimináció szabálya elfogadható. Ezt az eredményt Gentzen főtételének (Hauptsatz) is nevezik.^[2]^[3]

Variánsok

A fenti szabályok többféleképpen módosíthatók:

Kisebb szerkezeti alternatívák

A szekvensek és a strukturális szabályok formalizálásának technikai részleteiben van némi választási lehetőség. Mindaddig, amíg az LK minden levezetése az új szabályok használatával hatékonyan átalakítható deriválttá, és fordítva, a módosított szabályokat továbbra is LK-nak nevezhetjük.

Először is, mint már említettük, a szekvenshalmazokból, vagy multihalmazokból áll. Ebben az esetben a permutálás (halmazok használatakor) és a szerződési képletek szabályai elavultak.

A gyengülés szabálya akkor válik elfogadhatóvá, amikor az axiómát (I) megváltoztatják úgy, hogy a forma bármely szekvensére $\Gamma ,A\vdash A,\Delta$ következtetni tudjunk. Ez azt jelenti $A$ bármilyen összefüggésben bizonyítja $A$ -t. Bármely gyengülés, amely egy derivációban jelentkezik, azután azonnal elvégezhető. Ez kényelmes változást jelent a bizonyítások alulról felfelé történő összeállításakor.

Ezektől függetlenül megváltoztathatja a kontextusok szabályokon belüli felosztásának módját is: Az $({\land }R),({\lor }L)$ , és $({\rightarrow }L)$ esetekben a bal oldali összefüggés $\Gamma$ és $\Sigma$ részekre oszlik, amikor felfelé halad. Mivel a kontrakció lehetővé teszi ezek megkettőzését, feltételezhetjük, hogy a teljes kontextust használjuk a deriváció mindkét ágában. Ezzel biztosítani lehet, hogy a rossz ágban egyetlen fontos premissza sem veszik el. A gyengítés alkalmazásával a kontextus irreleváns részei később kiküszöbölhetők.

Abszurdum

Bevezetjük a $\bot$ -t, a hamisat képviselő abszurd konstanst az axiómával:

{\cfrac {}{\bot \vdash \quad }}

Vagy ha a fentiek szerint a gyengülés elfogadható szabály, akkor az axiómával:

{\cfrac {}{\Gamma ,\bot \vdash \Delta }}

$\bot$ esetén a tagadás az implikáció speciális eseteként felfogható a $\neg A\iff A\to \bot$ definíción keresztül.

Szubstrukturális logika

Alternatív megoldásként korlátozhatja vagy megtilthatja egyes szerkezeti szabályok alkalmazását. Ez különféle szubstrukturális logikai rendszereket eredményez. Általában gyengébbek, mint az LK ( vagyis kevesebb tételük van), és így nem teljesek az elsőrendű logika szokásos szemantikája szempontjából. Vannak azonban más érdekes tulajdonságaik, amelyek az elméleti számítástechnika és a mesterséges intelligencia alkalmazásához vezettek.

Intuicionista szekvenskalkulus: LJ rendszer

Meglepő módon néhány apró változtatás az LK szabályaiban elegendő ahhoz, hogy az intuíciós logika igazoló rendszerévé váljon.^[27] Ebből a célból olyan szekvensekre kell korlátozódni, amelyek legfeljebb egy formulával rendelkeznek a jobb oldalon, és módosítani kell a szabályokat, hogy ez a konstans maradjon. Például, $({\lor }L)$ -t a következőképpen fogalmazzák meg (ahol C jelentése tetszőleges képlet):

{\cfrac {\Gamma ,A\vdash C\qquad \Sigma ,B\vdash C}{\Gamma ,\Sigma ,A\lor B\vdash C}}\quad ({\lor }L)

A kapott rendszert LJ-nek hívják. Megalapozott és teljes az intuicionista logika szempontjából, és hasonló cut-eliminációs bizonyítást ismer el. Ez felhasználható a diszjunkció és a fennállás tulajdonságainak bizonyítására.

Valójában az LK egyetlen két szabálya, amelyet egyetlen képlet következményeire kell korlátozni, az $({\to }R)$ és $(\neg R)$ ^[28] (és ez utóbbi az előbbi speciális esetének tekinthető, mint $\bot$ , a fent leírtak szerint). Ha a több formulájú konzekvenseket disszjunkciókként interpretáljuk, az LK összes többi következtetési szabálya valóban levezethető LJ-ben, míg a szabálysértő szabály:

{\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}

Ez megegyezik a propozíciós formulával $(A\to (B\lor C))\to ((A\to B)\lor C)$ , ami egy klasszikus tautológia, amely konstruktívan nem érvényes.

Jegyzetek

↑ ^a ^b Gentzen 1934, Gentzen 1935.
↑ ^a ^b Curry 1977, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
↑ ^a ^b Kleene 2009, pp. 453, gives a very brief proof of the cut-elimination theorem.
↑ Curry 1977, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.
↑ Kleene 2009. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.
↑ Kleene 2002, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.
↑ Smullyan 1995, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.
↑ Curry 1977, pp. 184–244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.
↑ Suppes 1999, pp. 25–150, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.
↑ Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999, pp. 25–150.
↑ Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"
↑ Shankar: PVS Prover Guide (PDF). User guide. SRI International, 2001. november 1. (Hozzáférés: 2015. május 29.)
↑ For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977, pp. 189–190, Kleene 2002, pp. 290, 297, Kleene 2009, Hilbert & Bernays 1970, Smullyan 1995, pp. 104–105 and Gentzen 1934.
↑ Buss 1998
↑ Gentzen 1934, p. 188. "Der Kalkül NJ hat manche formale Unschönheiten."
↑ Gentzen 1934, p. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben."
↑ Gentzen 1934, p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."
↑ Gentzen 1934, p. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."
↑ Kleene 2002, p. 441.
↑ ^a ^b ^c Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25
↑ "Remember, the way that you prove an implication is by assuming the hypothesis."—Philip Wadler, on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip
↑ Gentzen's original consistency proof and the Bar Theorem, Gentzen's Centenary: The Quest for Consistency. New York: Springer, 213–228. o. (2010)
↑ Jan von Plato, Elements of Logical Reasoning, Cambridge University Press, 2014, p. 32.
↑ Gentzen 1934, 190–193. o.
↑ Smullyan 1995, p. 107
↑ Kleene 2002, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."
↑ Gentzen 1934, p. 194, wrote: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between intuitionistic and classical logic is in the case of the calculi LJ and LK of an extremely, totally different kind to the case of NJ and NK. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."
↑ Structural Proof Theory (CUP, 2001), Sara Negri and Jan van Plato

Hivatkozások

Buss, Samuel R..szerk.: Samuel R. Buss: An introduction to proof theory, Handbook of proof theory. Elsevier, 1–78. o. (1998). ISBN 0-444-89840-9
Curry, Haskell Brooks. Foundations of mathematical logic. New York: Dover Publications Inc. [1963] (1977). ISBN 978-0-486-63462-3
Gentzen (1934). „Untersuchungen über das logische Schließen. I”. Mathematische Zeitschrift 39 (2), 176–210. o. DOI:10.1007/BF01201353.
Gentzen (1935). „Untersuchungen über das logische Schließen. II”. Mathematische Zeitschrift 39 (3), 405–431. o. DOI:10.1007/bf01201363.
Girard, Jean-Yves. Proofs and Types. Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 7) [1989] (1990). ISBN 0-521-37181-3
Hilbert, David. Grundlagen der Mathematik II, Second, Berlin, New York: Springer-Verlag [1939] (1970). ISBN 978-3-642-86897-9
Kleene, Stephen Cole. Introduction to metamathematics. Ishi Press International [1952] (2009). ISBN 978-0-923891-57-2
Kleene, Stephen Cole. Mathematical logic. Mineola, New York: Dover Publications [1967] (2002). ISBN 978-0-486-42533-7
Lemmon, Edward John. Beginning logic. Thomas Nelson (1965). ISBN 0-17-712040-1
Smullyan, Raymond Merrill. First-order logic. New York: Dover Publications [1968] (1995). ISBN 978-0-486-68370-6
Suppes, Patrick Colonel. Introduction to logic. Mineola, New York: Dover Publications [1957] (1999). ISBN 978-0-486-40687-9

Fordítás

Ez a szócikk részben vagy egészben a Sequent calculus című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

További információk

Kapcsolódó szócikk

Rezolúció

[gentzen19341935-1] Gentzen 1934, Gentzen 1935.

[curry_cut_elimination-2] Curry 1977, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.

[kleene_cut_elimination-3] Kleene 2009, pp. 453, gives a very brief proof of the cut-elimination theorem.

[4] Curry 1977, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.

[5] Kleene 2009. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.

[6] Kleene 2002, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.

[7] Smullyan 1995, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.

[8] Curry 1977, pp. 184–244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.

[9] Suppes 1999, pp. 25–150, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.

[10] Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999, pp. 25–150.

[11] Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"

[pvs-prover-12] Shankar: PVS Prover Guide (PDF). User guide. SRI International, 2001. november 1. (Hozzáférés: 2015. május 29.)

[13] For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977, pp. 189–190, Kleene 2002, pp. 290, 297, Kleene 2009, Hilbert & Bernays 1970, Smullyan 1995, pp. 104–105 and Gentzen 1934.

[14] Buss 1998

[15] Gentzen 1934, p. 188. "Der Kalkül NJ hat manche formale Unschönheiten."

[16] Gentzen 1934, p. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben."

[17] Gentzen 1934, p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."

[18] Gentzen 1934, p. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."

[19] Kleene 2002, p. 441.

[Cornell09-20] Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25

[Wadler-21] "Remember, the way that you prove an implication is by assuming the hypothesis."—Philip Wadler, on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip

[Tait-22] Gentzen's original consistency proof and the Bar Theorem, Gentzen's Centenary: The Quest for Consistency. New York: Springer, 213–228. o. (2010)

[23] Jan von Plato, Elements of Logical Reasoning, Cambridge University Press, 2014, p. 32.

[FOOTNOTEGentzen1934190–193-24] Gentzen 1934, 190–193. o.

[25] Smullyan 1995, p. 107

[26] Kleene 2002, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."

[27] Gentzen 1934, p. 194, wrote: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between intuitionistic and classical logic is in the case of the calculi LJ and LK of an extremely, totally different kind to the case of NJ and NK. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."

[28] Structural Proof Theory (CUP, 2001), Sara Negri and Jan van Plato

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]