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,, gives a 5-page proof of the elimination theorem. See also pages 188, 250., gives a very brief proof of the cut-elimination theorem. 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,, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs., defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem., gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style. é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
Ahol 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
ahol az és formulák és . Az permutációi nem lényegesek. Más szavakkal, egy ítélet egy formulából (esetleg üres formulából) áll a " " szimbólum (forgókereszt szimbólum) bal oldalán, és egyetlen formulából a jobb oldalon., compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical., is an introductory presentation of practical natural deduction of this kind. This became the basis of System L. is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on . A tételek azok a formulák, oly módon, hogy (üres bal oldallal) egy érvényes bizonyítás következtetése. (A természetes levezetés egyes bemutatásaiban az -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ármikorHere, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment" , stb., mind igazak, akkor is igaz lesz. Az ítéletek
és
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
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: és formulák, és 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 -k is, ahol egy érvényes bizonyíték következtetése.
Egy szekvens alapértelmezett szemantikája egy állítás, hogy amikor minden igaz, legalább egy is igaz lesz.For explanations of the disjunctive semantics for the right side of sequents, see , , , , and . Í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
és
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
(legalább az egyik A hamis, vagy az egyik B igaz) vagy
(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.. "Der Kalkül NJ hat manche formale Unschönheiten." 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.. "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." 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).. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener." 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.. "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."
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 bélyegkép|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.Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25
Vegyük figyelembe a következő formulát: