Sekvenční počet

Sekvenční kalkul je variantou logického kalkulu , která k dokazování tvrzení nepoužívá libovolné řetězce tautologií , ale posloupnosti podmíněných výroků - sekvencí . Nejznámější sekvenční kalkuly - a pro klasický a intuicionistický predikátový kalkul - sestrojil Gentzen v roce 1934 , později byly formulovány sekvenční varianty pro širokou třídu aplikovaných kalkulů (aritmetika, analýza), teorie typů, ne - klasická logika. $\mathbf {LK}$ $\mathbf {LJ}$

V sekvenčním přístupu se místo širokých souborů axiomů používají vyvinuté systémy inferenčních pravidel a důkaz je prováděn ve formě inferenčního stromu; na tomto základě (spolu se systémy přirozené inference ) jsou sekvenční kalkuly typu Gentzen , na rozdíl od axiomatických Hilbertových kalkulů , ve kterých je s rozvinutou sadou axiomů počet inferenčních pravidel redukován na minimální.

Hlavní vlastností sekvenční formy je symetrické zařízení , které poskytuje pohodlí při dokazování odstranitelnosti sekcí a v důsledku toho jsou sekvenční kalkuly hlavními systémy studovanými v teorii důkazů .

Historie

Pojem sequence pro systematické použití v důkazech ve formě derivačního stromu zavedl v roce 1929 německý fyzik a logik Paul Hertz ( německy: Paul Hertz ; 1881-1940) [1] , ale holistický kalkul pro jakýkoli logický teorie nebyla v jeho dílech postavena [2] . V práci z roku 1932 se Gentzen pokusil rozvinout Hertzův přístup [3] , ale v roce 1934 Hertzův vývoj opustil: zavedl přirozené inferenční systémy jak pro klasický, tak pro intuicionistický predikátový kalkul, s použitím běžných tautologií a inferenčních stromů, a jako např. jejich strukturální vývoj, — sekvenční systémy a . For and Gentzen prokázal odstranitelnost řezu, což dalo významný metodologický impuls teorii důkazu nastíněné Hilbertem: Gentzen v téže práci nejprve prokázal úplnost intuicionistického predikátového kalkulu a v roce 1936 prokázal konzistenci Peanova axiomatika pro celá čísla, rozšiřující ji pomocí sekvenční varianty o transfinitní indukci na ordinální . Posledně jmenovaný výsledek měl také zvláštní ideologický význam ve světle pesimismu počátku třicátých let v souvislosti s Gödelovou větou o neúplnosti , podle níž nelze konzistenci aritmetiky stanovit vlastními prostředky: dostatečně přirozené rozšíření aritmetiky o logiku bylo zjistil, že toto omezení eliminuje. $\mathbf {NK}$ $\mathbf {NJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {NK}$ $\epsilon_0$

Dalším významným krokem ve vývoji sekvenčního počtu byl vývoj v roce 1944 Oivou Ketonenem ( fin. Oiva Ketonen ; 1913-2000) počtu pro klasickou logiku, ve kterém jsou všechna pravidla odvození reverzibilní; zároveň Ketonen navrhl dekompoziční přístup k nalezení důkazů pomocí vlastnosti reverzibilita [4] [5] . Počet bez axiomů publikovaný v roce 1949 v dizertační práci Romana Sushka byl svou formou blízký Hertzovým konstrukcím a byl první inkarnací pro sekvenční systémy Hertzova typu [6] [7] .

V roce 1952 Stephen Kleene ve svém Úvodu do metamatematiky, založeném na Ketonenově kalkulu, zkonstruoval intuicionistický sekvenční kalkul s pravidly reverzibilní inference [8] , zavedl také kalkul Gentzenova typu a , který nevyžadoval strukturální inferenci . pravidla [9] , a obecně po vydání knihy se sekvenční kalkul stal známým v širokém okruhu odborníků [4] . $G3i$ $G3c$

Od 50. let byla hlavní pozornost věnována rozšíření výsledků o konzistenci a úplnosti na predikátové kalkuly vyššího řádu, teorii typů , neklasické logiky . V roce 1953 Gaishi Takeuchi (竹内外史; 1926–2017) zkonstruoval sekvenční počet pro jednoduchou teorii typů vyjadřující predikátový počet vyššího řádu a navrhl, že řezy jsou pro něj odstranitelné ( Takeuchiho domněnka ). V roce 1966 William Tate ( nar. 1929 ) prokázal odstranitelnost sekcí pro logiku druhého řádu , brzy byla domněnka plně prokázána v pracích Motoo Takahashi [10] a Dag Prawitz ( švéd . Dag Prawitz ; nar. 1936). V 70. letech byly výsledky výrazně rozšířeny: Dragalin našel důkazy odstranitelnosti sekcí pro řadu neklasických logik vyššího řádu a Girard pro systém F .

Od 80. let 20. století hrají sekvenční systémy klíčovou roli ve vývoji automatických důkazových systémů , zejména sekvenční počet konstrukcí vyvinutý Thierry Cocanem a Gerardem Huetem v roce 1986 je polymorfní λ-počet vyššího řádu se závislými typy , který zaujímá nejvyšší bod v λ-kostce Barendregt - použitý jako základ softwarového systému Coq .

Základní pojmy

Sequent je vyjádření tvaru, kdea jsou konečné (případně prázdné) sekvence logických vzorců, nazývané cedenty : - antecedent , a - succedent (někdy - důsledek ). Intuitivní význam stanovený v sequent je ten, že pokud se provede konjunkce předcházejících formulídojde (je odvozena) disjunkce následných formulí. Někdy se místo šipky v zápisu posloupnosti používá znaménko odvoditelnosti () nebo. $\Gamma \šipka doprava \Delta$ $\Gamma$ $\Delta$ $\Gamma$ $\Delta$ ${\displaystyle A_{1},\ldots ,A_{n}\rightarrow B_{1},\ldots ,B_{m))$ ${\displaystyle A_{1}\land \ldots \land A_{n))$ ${\displaystyle B_{1}\lor \ldots \lor B_{m))$ $\Gamma \vdash \Delta$ $\Gamma \Rightarrow \Delta$

Je-li antecedent prázdný ( ), pak je implikována disjunkce následných formulí ; prázdný sucedent ( ) je interpretován jako nekonzistence ve spojení předcházejících formulí. Prázdná sekvence znamená, že v posuzovaném systému existuje rozpor. Pořadí vzorců v cedantech není významné, ale na počtu výskytů instance vzorce v cedantu záleží. Záznam v přiřazovatelích ve tvaru nebo , kde je posloupnost vzorců a je vzorcem, znamená přidání vzorce k přiřazovateli (třeba ještě v jedné kopii). ${\displaystyle \rightarrow B_{1},\ldots ,B_{m))$ ${\displaystyle B_{1}\lor \ldots \lor B_{m))$ $A_{1},\ldots ,A_{n}\rightarrow$ $\šipka doprava$ $A,\Gamma$ $\Gamma ,A$ $\Gamma$ $A$ $A$

Axiómy jsou počáteční sekvence přijímané bez důkazu; v sekvenčním přístupu je počet axiomů minimalizován, takže v Gentzenově kalkulu je dáno pouze jedno schéma axiomů - . Odvozovací pravidla v sekvenční formě jsou zapsána jako následující výrazy: $\mathrm {LK}$ $\mathrm {LJ}$ $A\rightarrow A$

{\cfrac {\;S_{1}\;}{T))

a ,

{\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;\;T))

jsou interpretovány jako tvrzení o odvoditelnosti z horní posloupnosti (horní posloupnosti a ) z dolní posloupnosti . Důkaz v sekvenčním počtu (jako v systémech přirozené inference) se zapisuje ve stromové podobě shora dolů, například: $S_{1}$ $S_{1}$ $S_{2}$ $T$

{\cfrac {{\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;T_{1))}\;\;\;\;{\cfrac {\;S_{3}\;}{T_{2}}}}{U}}

kde každý řádek znamená přímou inferenci - přechod od horních sekvencí k nižším podle některého z inferenčních pravidel přijatých v daném systému. Existence inferenčního stromu vycházejícího z axiomů (počátečních sekvencí) a vedoucího k sekvenci tedy znamená jeho odvoditelnost v daném logickém systému: . $S$ $\vDash S$

Klasický Gentzenův sekvenční kalkul

Nejčastěji používaným sekvenčním kalkulem pro klasický predikátový kalkul je systém zkonstruovaný Gentzenem v roce 1934. Systém má jedno schéma axiomů – a 21 inferenčních pravidel, která se dělí na strukturální a logická [11] . $\mathbf {LK}$ $A\rightarrow A$

Strukturální pravidla (, — vzorce,,,, — seznamy vzorců): $A$ $B$ $\Gamma$ $\Delta$ $\Theta$ $\lambda$

útlum vlevo: a vpravo: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A))$
zkratka vlevo: a vpravo: ; ${\cfrac {\,\,A,\ A,\ \Gamma \ \rightarrow \ \Delta }{\qquad A,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \\Delta ,\ A\qquad ))$
permutace vlevo: a vpravo: , ${\cfrac {\ \Gamma ,\ A,\ B,\ \Theta \ \\rightarrow \ \Delta \ }{\ \Gamma ,\ B,\ A,\ \Theta \ \rightarrow \ \Delta ))$ ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A,\ B,\ \Lambda \ }{\ \Gamma \ \rightarrow \ \Delta ,\ B,\ A,\ \Lambda \ } }$
sekce : . ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ Lambda }}$

Logická výroková pravidla jsou navržena tak, aby k výstupu přidala výrokové spojky :

$\lne$ -vlevo: ; -vpravo: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad ))$ $\lne$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ ))$
$\přistát$ -vlevo: a ; -vpravo: , ${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ $\přistát$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$
$\lor$ -vlevo: ; -vpravo : a $\ {\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad B,\ \Gamma \ \rightarrow \ \Delta \ }{\ A\lor B,\ \Gamma \ \rightarrow \ \Delta \ \qquad}}$ $\lor$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ A\lor B\ ))$ ${\cfrac {\Gamma \rightarrow \Delta ,\ B\qquad }{\ \Gamma \rightarrow \Delta ,\ A\lor B\ ))$
$\Šipka doprava$ -vlevo : a -vpravo: . $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$ $\Šipka doprava$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta,\ A\Rightarrow B\ ))$

Pravidla logických kvantifikátorů zavádějí do derivace kvantifikátory univerzálnosti a existence ( je vzorec s volnou proměnnou , je libovolný termín a je nahrazením všech výskytů volné proměnné termínem ): $F(a)$ $A$ $t$ $F(t)$ $A$ $t$

$\pro všechny$ -left : a -right: ; ${\cfrac {\qquad F(t),\ \Gamma \ \rightarrow \ \Delta }{\ \forall x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\pro všechny$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\ \Gamma \ \rightarrow \ \Delta,\ \forall x:F(x)))$
$\existuje$ -vlevo : a -vpravo: . ${\cfrac {\qquad F(a),\ \Gamma \ \rightarrow \ \Delta }{\ \exists x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\existuje$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(t)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \exists x:F(x)))$

Další podmínkou v pravidlech kvantifikátoru je nevyskytování se volné proměnné ve vzorcích nižších sekvencí v pravidlech -vpravo a Vlevo . $A$ $\pro všechny$ $\existuje$

Příklad odvození zákona vyloučeného středu : $\mathbf {LK}$

{\cfrac {\cfrac {\cfrac {\cfrac {\cfrac {A\ \rightarrow \ A\qquad }{\qquad \quad \rightarrow \ A,\ \lne A\qquad )){\qquad \ qquad \rightarrow \ A,\ A\lor \lnot A\quad }}{\qquad \quad \rightarrow \ A\lor \lnot A,\ A}}{\qquad \qquad \qquad \ \rightarrow \ A\lor \lne A,\ A\nebo \lne A\quad }}{\quad \ \rightarrow \ A\nebo \lnot A}}

- v něm začíná odvozování jediným axiomem, pak - se postupně uplatňují pravidla -pravá, -pravá, permutace vpravo, -pravá a redukce vpravo. $\lne$ $\lor$ $\lor$

Počet je ekvivalentní klasickému predikátovému počtu prvního stupně: formule platí v predikátovém počtu právě tehdy, když je sequent odvoditelný v . Klíčovým výsledkem, který Gentzen nazval „ hlavní teorém “ ( německy Hauptsatz ), je schopnost provádět jakoukoli inferenci bez použití pravidla řezu, díky této vlastnosti jsou stanoveny všechny základní vlastnosti , včetně správnosti , konzistence a úplnost. $\mathbf {LK}$ $A$ $\mathbf {LK}$ $\rightarrow A$ $\mathbf {LK}$ $\mathbf {LK}$

Gentzenův intuicionistický sekvenční kalkul

Počet se získá přidáním omezení na následníky sekvencí v pravidlech odvozování: je v nich povolen pouze jeden vzorec a pravidla pravé permutace a pravé redukce (operace s několika formulemi v sukcesích) jsou vyloučena. S minimálními úpravami je tedy získán systém, ve kterém nejsou odvoditelné zákony dvojí negace a vyloučené tercie , ale platí všechny ostatní základní logické zákony a např. ekvivalence je odvoditelná . Výsledný systém je ekvivalentní intuicionistickému predikátovému počtu s Heytingovou axiomatikou . Sekce jsou odstranitelné i v kalkulu , je také správný, konzistentní a úplný, navíc poslední výsledek pro intuicionistický predikátový kalkul byl poprvé získán právě pro . $\mathbf {LJ}$ $\mathbf {LK}$ $\lnot \lnot \lnot A\Leftrightarrow \lnot A$ $\mathbf {LJ}$ $\mathbf {LJ}$

Nestandardní sekvenční kalkuly

Bylo vytvořeno velké množství ekvivalentních a vhodných variant sekvenčního počtu pro klasické a intuicionistické logiky. Některé z těchto kalkulů zdědí Gentzenovu konstrukci použitou při dokazování konzistence Peanovy aritmetiky a zahrnují prvky systémů přirozeného odvozování, mezi nimi systém Sapps ( Patrick Suppes ; 1922–2014) z roku 1957 [12] (převzato z Feisových poznámek a Ladrière do francouzského překladu Gentzenova článku) a jeho vylepšené verze publikované v roce 1965 Johnem Lemmonem ( 1930-1966 ) [13] , eliminující praktické nepohodlí používání Gentzenova originálu Nutral Sequential [14] . Radikálnější vylepšení pro praktickou výhodnost odvozování přírodních typů v sekvenčním kalkulu navrhl Hermes ( německy: Hans Hermes ; 1912-2003) [15] : v jeho systému pro klasickou logiku se uplatňují dva axiomy ( a , a v pravidlech z inference se výroková spojení používají nejen v sucedentech, ale i v antecedentech, navíc jak v nižších, tak v horních sekvencích [16] . $A\rightarrow A$ $\rightarrow A=A$

Symetrie

Sekvenční kalkul je vlastní symetrii, přirozeně vyjadřující dualitu , v axiomatických teoriích formulovaných de Morganovými zákony .

Poznámky

↑ Hertz P. Über Axiomensysteme für beliebige Satzsysteme (německy) // Mathematische Annalen. - 1929. - Bd. 101 . - S. 457-514 . - doi : 10.1007/BF01454856 .
↑ Indrzejczak, 2014 , Hertz nepředložil žádný konkrétní systém pro konkrétní logiku. Jeho přístup byl abstraktní; definoval spíše schéma systému, ve kterém mají jediná pravidla čistě strukturální charakter, s. 1310.
↑ Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (německy) // Mathematische Annalen. - 1932. - Bd. 107 . — S. 329–350 . - doi : 10.1007/BF01448897 .
↑ 1 2 Jan von Plateau, 2008 .
↑ Bernays P. Recenze: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (anglicky) // Journal of Symbolic Logic . - 1945. - Sv. 10 , č. 4 . - S. 127-130 .
↑ Suszko R. Formalna teoria wartości logicznych (polsky) // Studia Logica. - 1957. - T. 6 . — S. 145–320 .
↑ Indrzejczak, 2014 , 1310-1315, s. 1310.
↑ Kleene, 1958 , str. 389-406.
↑ Kleene, 1958 , str. 424-434.
↑ Takahashi M. A proof of cut-elimination theorem in simple type-theory // Journal of Japanese Mathematical Society. - 1967. - T. 19 , č. 4 . - S. 399-410 . - doi : 10.2969/jmsj/01940399 .
↑ Takeuchi, 1978 .
↑ Suppes P. Úvod do logiky. Princeton: Van Nostrand, 1957.
↑ Lemmon EJ Počáteční logika. — Londýn: Nelson, 1965.
↑ Indrzejczak, 2014 , str. 1300.
↑ Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
↑ Indrzejczak, 2014 , <...> pro získání flexibilnějšího nástroje pro aktuální vyhledávání důkazů lze připustit možnost provádění logických operací i v předchůdcích. <…> Zdá se, že první systém tohoto druhu poskytl Hermes. Ve své formalizaci klasické logiky s identitou používá také intuicionistické sekvence se sekvencemi formulí v předchůdcích. Jako primitivní sekvence Hermes používá pouze: a , s. 1300. $\varphi \Rightarrow \varphi$ $\Rightarrow \tau =\tau$

Literatura

Sekvenční kalkul // Safflower - Soan. - M .: Sovětská encyklopedie, 1976. - S. 181-182; Umění. 530-532. - ( Velká sovětská encyklopedie : [ve 30 svazcích] / šéfredaktor A. M. Prochorov ; 1969-1978, v. 23).
Dragalin A. G. Sekvenční počet // Mathematical Encyclopedia : [v 5 svazcích] / Ch. vyd. I. M. Vinogradov . - M . : Sovětská encyklopedie, 1984. - T. 4: Dobře - Slo. - S. 1104. - 1216 stb. : nemocný. — 150 000 výtisků.
Bystrov P.I. Sekvenční počet // Nová filozofická encyklopedie / Filosofický ústav RAS ; Národní společensko-vědní fond; Předchozí vědecky vyd. rada V. S. Stepin , místopředsedové: A. A. Guseynov , G. Yu. Semigin , účetní. tajný A. P. Ogurtsov . — 2. vyd., opraveno. a přidat. - M .: Myšlenka , 2010. - ISBN 978-5-244-01115-9 .
Gentzen G. Inference Studies = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Idelson A. V., Mints G. E. Mathematical theory of inference / přeložil A. V. Idelson. - M .: Nauka, 1967. - S. 9-76 .
Dragalin A.G. Matematický intuicionismus. Úvod do teorie důkazů. — M .: Nauka , 1979. — 256 s. — (Matematická logika a základy matematiky).
Kleene S. Introduction to Metamathematics / překlad z angličtiny A. S. Yesenin-Volpin , editoval V. A. Uspenskij . - M. : IL, 1958. - 527 s.
Takeuchi G. Teorie důkazu. - M .: Mir, 1978. - 412 s.
Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica . - 2014. - prosinec ( roč. 102 , č. 6 ). - S. 1295-1322 . - doi : 10.1007/s11225-014-9567-y .
Jan von Plato. Vývoj teorie důkazu . Stanford Encyclopaedia of Philosophy (16. dubna 2008). (neurčitý)

Logika

Filosofie • Sémantika • Syntaxe • Historie

Logické skupiny

klasická logika	Aristotelská logika výroková logika Logika prvního řádu Logika druhého řádu logika vyššího řádu
matematická logika	teorie množin Teorie modelu Teorie vyčíslitelnosti Důkazová teorie a konstruktivní matematika Lineární logika formální systém přirozený závěr Sekvenční počet Algebra logiky Relevantní logika Deontická logika intuicionistická logika Lambekův počet
Neklasická logika	intuicionismus fuzzy logika Substrukturální logika logika Popisná logika Vícehodnotová logika Logická syntéza Závazná logika Temporální logika Modální logika ( Hybrid logic ) epistemická logika
Filosofická logika	Kritické myšlení neformální logika deduktivní uvažování

Komponenty

Seznam booleovských symbolů