Sekvenskalkyl

Sekvenskalkyl är en variant av logisk kalkyl som inte använder godtyckliga kedjor av tautologier för att bevisa påståenden , utan sekvenser av villkorliga propositioner - sekvenser . De mest kända sekvenskalkylerna - och för den klassiska och intuitionistiska predikatkalkylen - byggdes av Gentzen 1934 , senare sekvensvarianter formulerades för en bred klass av tillämpade kalkyler (aritmetik, analys), typteorier, icke - klassisk logik. $\mathbf {LK}$ $\mathbf {LJ}$

I det sekventiella tillvägagångssättet, istället för breda uppsättningar av axiom , används utvecklade system av slutledningsregler , och beviset utförs i form av ett slutledningsträd; på denna grund (tillsammans med system av naturlig inferens ) är sekventiella kalkyler av Gentzen-typ , i motsats till den axiomatiska Hilbert-kalkylen , där antalet inferensregler reduceras till en utvecklad uppsättning axiom. minimum.

Huvudegenskapen för den sekventiella formen är den symmetriska enheten , som ger bekvämligheten att bevisa borttagningsbarheten av sektioner , och som ett resultat är sekventiella kalkyler de huvudsakliga systemen som studeras i bevisteori .

Historik

Konceptet med en sekvens för systematisk användning i bevis i form av ett härledningsträd introducerades 1929 av den tyske fysikern och logikern Paul Hertz ( tyska: Paul Hertz ; 1881-1940) [1] , men en holistisk kalkyl för alla logiska teori byggdes inte i hans verk [2] . I arbetet från 1932 försökte Gentzen utveckla Hertz tillvägagångssätt [3] , men 1934 övergav han Hertz utveckling: han introducerade naturliga slutledningssystem för både den klassiska respektive intuitionistiska predikatkalkylen, med hjälp av vanliga tautologier och inferensträd, och som deras strukturella utveckling. — Sekventiella system och . For och Gentzen bevisade att snittet kunde avlägsnas, vilket gav en betydande metodologisk impuls till bevisteorin som skisserades av Hilbert: i samma arbete bevisade Gentzen först fullständigheten av den intuitionistiska predikatkalkylen, och 1936 bevisade han konsekvensen av Peanos axiomatik för heltal, förlängning av den med hjälp av en sekventiell variant genom transfinit induktion till ordinal . Det sistnämnda resultatet hade också en speciell ideologisk betydelse i ljuset av pessimismen i början av 1930-talet i samband med Gödels ofullständighetssats , enligt vilken aritmetikens konsistens inte kan fastställas med egna medel: en tillräckligt naturlig förlängning av aritmetiken med logiken var funnit att denna begränsning elimineras. $\mathbf {NK}$ $\mathbf {NJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {NK}$ $\epsilon_0$

Nästa betydande steg i utvecklingen av sekventiell kalkyl var utvecklingen 1944 av Oiva Ketonen ( fin. Oiva Ketonen ; 1913-2000) av en kalkyl för klassisk logik, där alla slutledningsregler är reversibla; samtidigt föreslog Ketonen en nedbrytningsmetod för att hitta bevis med hjälp av reversibilitetsegenskapen [4] [5] . Den axiomfria kalkylen som publicerades 1949 i Roman Sushkos avhandling var i form nära Hertz konstruktioner, och var den första inkarnationen för sekventiella system av Hertz-typ [6] [7] .

År 1952 konstruerade Stephen Kleene , i sin Introduction to Metamathematics, baserad på Ketonenkalkylen, en intuitionistisk sekvenskalkyl med reversibla slutledningsregler [8] , han introducerade även Gentzen-typkalkylen och , som inte krävde strukturell inferens regler [9] , och i allmänhet, efter publiceringen av boken, blev sekventiell kalkyl känd i en bred krets av specialister [4] . $G3i$ $G3c$

Sedan 1950-talet har den huvudsakliga uppmärksamheten ägnats åt utvidgningen av resultat om konsistens och fullständighet till högre ordningens predikatkalkyler, typteori , icke-klassisk logik . År 1953 konstruerade Gaishi Takeuchi (竹内外史; 1926–2017) en sekventiell kalkyl för en enkel typteori som uttrycker högre ordningens predikatkalkyl och föreslog att snitt är borttagbara för den ( Takeuchis gissning ). År 1966 bevisade William Tate ( f. 1929 ) möjligheten att avlägsna sektioner för andra ordningens logik , snart bevisades gissningen fullt ut i verken av Motoo Takahashi [10] och Dag Prawitz ( Svenska Dag Prawitz ; f. 1936). På 1970-talet utökades resultaten avsevärt: Dragalin hittade bevis för att sektioner kunde tas bort för en serie icke-klassiska logiker av högre ordning, och Girard för systemet F .

Sedan 1980-talet har sekventiella system spelat en nyckelroll i utvecklingen av automatiska bevissystem , i synnerhet är sekvenskalkylen av konstruktioner som utvecklades av Thierry Cocan och Gerard Huet 1986 en högre ordningens polymorf λ-kalkyl med beroende typer som upptar den högsta punkten i λ-kuben Barendregt - används som grund för Coqs mjukvarusystem .

Grundläggande begrepp

En sekvent är ett uttryck för formen, däroch är ändliga (möjligen tomma) sekvenser av logiska formler, kallade cedenter : - antecedent , och - succedent (ibland - konsekvent ). Den intuitiva betydelsen som fastställs i efterföljande är att om konjunktionen av de föregående formlernasker (härleds) disjunktionen av de efterföljande formlerna. Ibland, istället för en pil i notationen av en sekvens, används härledningstecknet () eller implikationstecknet (). $\Gamma \rightarrow \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$

Om antecedenten är tom ( ), så är disjunktionen av de efterföljande formlerna underförstådd ; en tom succedent ( ) tolkas som en inkonsekvens i konjunktionen av antecedentformler. En tom sekvens betyder att det finns en motsättning i det aktuella systemet. Ordningen på formler i cedanter är inte signifikant, men antalet förekomster av en formelinstans i en cedant har betydelse. Att spela in i tilldelare i formen eller , där är en sekvens av formler, och är en formel, innebär att lägga till en formel till tilldelaren (kanske i ytterligare en kopia). ${\displaystyle \rightarrow B_{1},\ldots ,B_{m))$ ${\displaystyle B_{1}\lor \ldots \lor B_{m))$ $A_{1},\ldots ,A_{n}\rightarrow$ $\höger pil$ $A,\Gamma$ $\Gamma ,A$ $\Gamma$ $A$ $A$

Axiom är initiala sekvenser accepterade utan bevis; i det sekventiella tillvägagångssättet är antalet axiom minimerat, så i Gentzens kalkyl ges endast ett schema av axiom - . Slutledningsregler i sekventiell form skrivs som följande uttryck: $\mathrm {LK}$ $\mathrm {LJ}$ $A\rightarrow A$

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

och ,

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

de tolkas som ett påstående om deducerbarheten från den övre sekvensen (övre sekvensen och ) av den nedre sekvensen . Bevis i sekventiell kalkyl (som i system med naturlig slutledning) skrivs i trädform uppifrån och ned, till exempel: $S_{1}$ $S_{1}$ $S_{2}$ $T$

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

där varje rad betyder en direkt slutledning - en övergång från de övre sekvenserna till de lägre enligt någon av de slutledningsregler som antagits i det givna systemet. Sålunda, förekomsten av ett slutledningsträd som utgår från axiom (initiala sekvenser) och leder till en sekvens betyder dess härledning i ett givet logiskt system: . $S$ $\vDash S$

Klassisk Gentzen sekvenskalkyl

Den vanligaste sekvenskalkylen för den klassiska predikatkalkylen är systemet som konstruerades av Gentzen 1934. Systemet har ett schema av axiom - och 21 slutledningsregler, som är uppdelade i strukturella och logiska [11] . $\mathbf {LK}$ $A\rightarrow A$

Strukturregler (, — formler,,,, — listor med formler): $A$ $B$ $\Gamma$ $\Delta$ $\Theta$ $\lambda$

dämpning vänster: och höger: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A))$
förkortning till vänster: och till höger: ; ${\cfrac {\,\,A,\ A,\ \Gamma \ \rightarrow \ \Delta }{\qquad A,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \Delta ,\ A\qquad ))$
permutation vänster: och höger: , ${\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 \ } }$
avsnitt :. _ ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ Lambda }}$

Logiska propositionsregler är utformade för att lägga till propositionella kopplingar till utdata :

$\linte$ -vänster: ; -höger: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad ))$ $\linte$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ ))$
$\landa$ -vänster: och ; -höger: , ${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ $\landa$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$
$\lor$ -vänster: ; -höger : och $\ {\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\ ))$
$\Höger pil$ -vänster: och -höger: . $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$ $\Höger pil$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ A\Rightarrow B\ ))$

Logiska kvantifierare regler introducerar universalitet och existenskvantifierare i härledningen ( är en formel med en fri variabel , är en godtycklig term och ersätter alla förekomster av en fri variabel med en term ): $F(a)$ $a$ $t$ $Med)$ $a$ $t$

$\för alla$ -vänster: och -höger: ; ${\cfrac {\qquad F(t),\ \Gamma \ \rightarrow \ \Delta }{\ \forall x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\för alla$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \forall x:F(x)))$
$\existerar$ -vänster: och -höger: . ${\cfrac {\qquad F(a),\ \Gamma \ \högerpil \ \Delta }{\ \exists x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\existerar$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(t)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \exists x:F(x)))$

Ett ytterligare villkor i kvantifierarreglerna är att en fri variabel inte förekommer i de lägre efterföljande formlerna i -höger- och -vänsterreglerna. $a$ $\för alla$ $\existerar$

Ett exempel på härledningen av lagen för den uteslutna mitten : $\mathbf {LK}$

{\cfrac {\cfrac {\cfrac {\cfrac {\cfrac {A\ \rightarrow \ A\qquad }{\qquad \quad \rightarrow \ A,\ \lnot 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 \lnot A,\ A\lor \lnot A\quad }}{\quad \ \rightarrow \ A\lor \lnot A}}

- i den börjar härledningen med ett enda axiom, sedan tillämpas - reglerna -höger, -höger, permutation till höger, -höger och reduktion till höger successivt. $\linte$ $\lor$ $\lor$

Kalkylen är ekvivalent med den klassiska predikatkalkylen för det första steget: en formel är giltig i predikatkalkylen om och endast om sekvensen är härledbar i . Nyckelresultatet, som Gentzen kallade " huvudsatsen " ( tyska Hauptsatz ) är förmågan att utföra vilken slutledning som helst utan att tillämpa skärningsregeln, det är tack vare denna egenskap som alla grundläggande egenskaper etableras , inklusive korrekthet , konsistens och fullständighet. $\mathbf {LK}$ $A$ $\mathbf {LK}$ $\rightarrow A$ $\mathbf {LK}$ $\mathbf {LK}$

Gentzens intuitionistiska sekvenskalkyl

Kalkylen erhålls genom att lägga till en begränsning av följderna av sekvenser i slutledningsreglerna: endast en formel är tillåten i dem, och reglerna för rätt permutation och rätt reduktion (som fungerar med flera formler i efterföljande) är exkluderade. Således, med minimala modifieringar, erhålls ett system där lagarna för dubbel negation och den uteslutna tredjedelen inte är härledbara , utan alla andra grundläggande logiska lagar gäller, och till exempel ekvivalens kan härledas . Det resulterande systemet är ekvivalent med den intuitionistiska predikatkalkylen med Heytings axiomatik . Sektioner är också borttagbara i kalkylen , den är också korrekt, konsekvent och komplett, dessutom erhölls det sista resultatet för den intuitionistiska predikatkalkylen först just för . $\mathbf {LJ}$ $\mathbf {LK}$ $\lnot \lnot \lnot A\Leftrightarrow \lnot A$ $\mathbf {LJ}$ $\mathbf {LJ}$

Icke-standardiserade sekvensberäkningar

Ett stort antal ekvivalenta och bekväma varianter av sekvenskalkyl för klassisk och intuitionistisk logik har skapats. Några av dessa kalkyler ärver Gentzen-konstruktionen som användes för att bevisa konsistensen av Peano-aritmetik och inkluderar element av system av naturlig härledning, bland dem Sapps- systemet ( Patrick Suppes ; 1922–2014) från 1957 [12] (hämtat från Feis kommentarer och Ladrière till den franska översättningen av Gentzens tidning) och dess förbättrade version publicerad 1965 av John Lemmon ( 1930-1966 ) [13] , vilket eliminerar det praktiska besväret med att använda Gentzens ursprungliga Nutral Sequential [14] . Mer radikala förbättringar för den praktiska bekvämligheten av naturtypinferens i sekventiell kalkyl föreslogs av Hermes ( tyska: Hans Hermes ; 1912-2003) [15] : i hans system för klassisk logik tillämpas två axiom ( och , och i reglerna av slutledning används propositionella bindeord inte bara i efterföljande utan också i antecedenter, dessutom, både i den nedre och i de övre sekvenserna [16] . $A\rightarrow A$ $\rightarrow A=A$

Symmetri

Sekventiell kalkyl är inneboende i symmetri, som naturligt uttrycker dualitet , i axiomatiska teorier formulerade av de Morgans lagar .

Anteckningar

↑ Hertz P. Über Axiomensysteme für beliebige Satzsysteme (tyska) // Mathematische Annalen. - 1929. - Bd. 101 . - S. 457-514 . - doi : 10.1007/BF01454856 .
↑ Indrzejczak, 2014 , Hertz presenterade inte något specifikt system för konkret logik. Hans tillvägagångssätt var abstrakt; han definierade snarare ett schema av systemet där de enda reglerna har en rent strukturell karaktär, sid. 1310.
↑ Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (tyska) // Mathematische Annalen. - 1932. - Bd. 107 . — S. 329–350 . - doi : 10.1007/BF01448897 .
↑ 1 2 Jan von Plateau, 2008 .
↑ Bernays P. Recension: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (engelska) // Journal of Symbolic Logic . - 1945. - Vol. 10 , nej. 4 . - S. 127-130 .
↑ Suszko R. Formalna teoria wartości logicznych (polska) // Studia Logica. - 1957. - T. 6 . — S. 145–320 .
↑ Indrzejczak, 2014 , 1310-1315, sid. 1310.
↑ Kleene, 1958 , sid. 389-406.
↑ Kleene, 1958 , sid. 424-434.
↑ Takahashi M. A proof of cut-elimination theorem in simple type-theory // Journal of Japanese Mathematical Society. - 1967. - T. 19 , nr 4 . - S. 399-410 . - doi : 10.2969/jmsj/01940399 .
↑ Takeuchi, 1978 .
↑ Suppes P. Introduktion till logik. Princeton: Van Nostrand, 1957.
↑ Lemmon EJ början logik. — London: Nelson, 1965.
↑ Indrzejczak, 2014 , sid. 1300.
↑ Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
↑ Indrzejczak, 2014 , <...> för att få ett mer flexibelt verktyg för faktisk bevissökning kan man medge möjligheten att göra logiska operationer även i antecedent. <…> Det verkar som om det första systemet av detta slag tillhandahålls av Hermes. Han använder också intuitionistiska sekvenser med sekvenser av formler i antecedent i sin formalisering av klassisk logik med identitet. Som primitiva sekvenser använder Hermes endast: och , sid. 1300. $\varphi \Rightarrow \varphi$ $\Rightarrow \tau =\tau$

Litteratur

Sekvenskalkyl // Safflor - Soan. - M .: Soviet Encyclopedia, 1976. - S. 181-182; Konst. 530-532. - ( Great Soviet Encyclopedia : [i 30 volymer] / chefredaktör A. M. Prokhorov ; 1969-1978, v. 23).
Dragalin A. G. Sekvenskalkyl // Mathematical Encyclopedia : [i 5 volymer] / Kap. ed. I. M. Vinogradov . - M . : Soviet Encyclopedia, 1984. - T. 4: Ok - Slo. - S. 1104. - 1216 stb. : sjuk. — 150 000 exemplar.
Bystrov P.I. Sequence Calculus // New Philosophical Encyclopedia / Institute of Philosophy RAS ; Nationell samhällsvetenskaplig fond; Föreg. vetenskaplig-ed. råd V. S. Stepin , vice ordförande: A. A. Guseynov , G. Yu. Semigin , revisor. hemlighet A.P. Ogurtsov . — 2:a uppl., rättad. och lägg till. - M .: Thought , 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 / översatt av A. V. Idelson. - M . : Nauka, 1967. - S. 9-76 .
Dragalin A. G. Matematisk intuitionism. Introduktion till bevisteori. — M .: Nauka , 1979. — 256 sid. — (Matematisk logik och matematikens grunder).
Kleene S. Introduction to Metamathematics / översättning från engelska av A. S. Yesenin-Volpin , redigerad av V. A. Uspensky . - M. : IL, 1958. - 527 sid.
Takeuchi G. Bevisteori. - M . : Mir, 1978. - 412 sid.
Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica . - 2014. - December ( vol. 102 , nr 6 ). - S. 1295-1322 . - doi : 10.1007/s11225-014-9567-y .
Jan von Platon. Utvecklingen av bevisteori . Stanford Encyclopaedia of Philosophy (16 april 2008). (obestämd)

Logik

Filosofi • Semantik • Syntax • Historia

Logiska grupper

klassisk logik	Aristotelisk logik propositionell logik Första beställningslogik Andra ordningens logik högre ordningslogik
matematisk logik	mängdteori Modellteori Beräkningsbarhetsteori Bevisteori och konstruktiv matematik Linjär logik formellt system naturlig slutsats Sekvenskalkyl Algebra av logik Relevant logik Deontisk logik intuitionistisk logik Lambek kalkyl
Icke-klassisk logik	intuitionism rolig logik Substrukturell logik logik Beskrivningslogik Flervärdig logik Logisk syntes Bindande logik Temporal logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritiskt tänkande informell logik deduktiva resonemang

Komponenter

Bortförande (logik)
Sannolikhet
påstående
Avdrag / Induktion / Traduktion
Verklighet
induktivt resonemang
slutledning
boolesk konstant
Sann
logiskt följa
Logisk form
Nödvändiga och tillräckliga förutsättningar
Beskrivning
Definition
Utbyte
Paket
Kontrovers ( Antinomy )
Syntetisk bedömning / Analytisk bedömning
Länk

Lista över booleska symboler