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 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, 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, é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. 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 $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. Ú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. Így az üres sorozat, amelynek mindkét szekvense üres, hamis. 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. 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. 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). 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.

A "szekvens" szó eredete

A "szekvencia" szót a "Sequenz" szóból vettük át Gentzen 1934-es cikkében. 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'."

Logikai formulák bizonyítása

Gyökeres fa, amely szekvenskalkulussal írja le a bizonyítási eljárást

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.

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

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.

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.

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”.) 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$, és $\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)$ $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$         $(\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.

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

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

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. 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)$ (é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.

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

• A Brief Diversion: Sequent Calculus
• Interactive tutorial of the Sequent Calculus

Kapcsolódó szócikk

• Rezolúció