Sekvensberegning

Sekvensregning er en variant af logisk kalkulus , der ikke bruger vilkårlige kæder af tautologier til at bevise udsagn , men sekvenser af betingede propositioner - sekvenser . De mest berømte sekventielle beregninger - og for den klassiske og intuitionistiske prædikatregning - blev bygget af Gentzen i 1934 , senere sekventielle varianter blev formuleret for en bred klasse af anvendte kalkuler (aritmetik, analyse), typeteorier, ikke - klassisk logik. $\mathbf {LK}$ $\mathbf {LJ}$

I den sekventielle tilgang, i stedet for brede sæt af aksiomer , anvendes udviklede systemer af slutningsregler , og beviset udføres i form af et slutningstræ; på dette grundlag (sammen med systemer af naturlig inferens ), er sekvente kalkuler af Gentzen-typen , i modsætning til de aksiomatiske Hilbert-regninger , hvor antallet af inferensregler reduceres med et udviklet sæt af aksiomer til en minimum.

Hovedegenskaben ved den sekventielle form er den symmetriske enhed , som giver bekvemmeligheden ved at bevise, at sektioner kan fjernes , og som et resultat er sekventielle beregninger de vigtigste systemer, der studeres i bevisteori .

Historie

Konceptet med en sekvent til systematisk brug i beviser i form af et afledningstræ blev introduceret i 1929 af den tyske fysiker og logiker Paul Hertz ( tysk: Paul Hertz ; 1881-1940) [1] , men en holistisk beregning for enhver logisk teori blev ikke bygget i hans værker [2] . I arbejdet i 1932 forsøgte Gentzen at udvikle Hertz' tilgang [3] , men i 1934 opgav han Hertz' udvikling: han introducerede naturlige inferenssystemer for henholdsvis den klassiske og intuitionistiske prædikatregning ved at bruge almindelige tautologier og inferenstræer, og som deres strukturelle udvikling — sekventielle systemer og . For og Gentzen beviste, at snittet kunne fjernes, hvilket gav en betydelig metodologisk impuls til bevisteorien skitseret af Hilbert: i samme værk beviste Gentzen først fuldstændigheden af den intuitionistiske prædikatregning, og i 1936 beviste han sammenhængen i Peanos aksiomatik for heltal, udvide det ved hjælp af en sekventiel variant ved transfinit induktion til ordinal . Sidstnævnte resultat havde også en særlig ideologisk betydning i lyset af pessimismen i begyndelsen af 1930'erne i forbindelse med Gödels ufuldstændighedssætning , hvorefter aritmetikkens konsistens ikke kan fastslås med egne midler: en tilstrækkelig naturlig forlængelse af aritmetikken ved logik var fundet, at eliminerer denne begrænsning. $\mathbf {NK}$ $\mathbf {NJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {NK}$ $\epsilon_0$

Det næste væsentlige trin i udviklingen af sekventiel regning var udviklingen i 1944 af Oiva Ketonen ( fin. Oiva Ketonen ; 1913-2000) af en calculus for klassisk logik, hvor alle slutningsregler er reversible; på samme tid foreslog Ketonen en nedbrydningstilgang til at finde bevis ved hjælp af reversibilitetsegenskaben [4] [5] . Den aksiomfrie kalkulus, der blev offentliggjort i 1949 i Roman Sushkos afhandling, var formmæssigt tæt på Hertz' konstruktioner, idet den var den første inkarnation for sekventielle systemer af Hertz-type [6] [7] .

I 1952 konstruerede Stephen Kleene i sin Introduction to Metamathematics, baseret på Ketonen-regningen, en intuitionistisk sekvensregning med reversible inferensregler [8] , han introducerede også Gentzen-typen og , som ikke krævede strukturel inferens regler [9] , og i det hele taget, efter udgivelsen af bogen, blev følgeregning kendt i en bred kreds af specialister [4] . $G3i$ $G3c$

Siden 1950'erne har hovedopmærksomheden været rettet mod udvidelsen af resultater om konsistens og fuldstændighed til højere ordens prædikatregning, typeteori , ikke-klassiske logikker . I 1953 konstruerede Gaishi Takeuchi (竹内外史; 1926–2017) en sekventiel beregning for en simpel typeteori, der udtrykker prædikatregning af højere orden, og foreslog, at nedskæringer kan fjernes for det ( Takeuchis formodning ). I 1966 beviste William Tate ( f. 1929 ) muligheden for at fjerne sektioner til andenordens logik , snart blev formodningen fuldt ud bevist i værkerne af Motoo Takahashi [10] og Dag Prawitz ( Sverige Dag Prawitz ; f. 1936). I 1970'erne blev resultaterne udvidet betydeligt: Dragalin fandt beviser for, at sektioner kunne fjernes for en række ikke-klassiske logikker af højere orden, og Girard for systemet F .

Siden 1980'erne har sekventielle systemer spillet en nøglerolle i udviklingen af automatiske bevissystemer , især den sekventielle beregning af konstruktioner udviklet af Thierry Cocan og Gerard Huet i 1986 er en højere ordens polymorf λ-regning med afhængige typer , der optager det højeste punkt i λ-kuben Barendregt - brugt som grundlag for Coq -softwaresystemet .

Grundlæggende begreber

En sekvent er et udtryk for formen, hvorog er endelige (muligvis tomme) sekvenser af logiske formler, kaldet cedenter : - antecedent , og - succedent (nogle gange - konsekvent ). Den intuitive betydning, der er fastlagt i den efterfølgende , er, at hvis konjunktionen af de forudgående formler udføres, så finder disjunktionen af de efterfølgende formlersted (afledes). Nogle gange bruges derivabilitetstegnet () eller implikationstegnet (. $\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$

Hvis antecedenten er tom ( ), så er disjunktionen af de efterfølgende formler underforstået ; en tom succedent ( ) fortolkes som en inkonsistens i sammenhængen af antecedentformler. En tom sekvens betyder, at der er en modsigelse i det undersøgte system. Rækkefølgen af formler i cedanter er ikke signifikant, men antallet af forekomster af en formelforekomst i en cedant betyder noget. Optagelse i tildelere i formen eller , hvor er en sekvens af formler, og er en formel, betyder at tilføje en formel til tildeleren (måske i en kopi mere). ${\displaystyle \rightarrow B_{1},\ldots ,B_{m))$ ${\displaystyle B_{1}\lor \ldots \lor B_{m))$ $A_{1},\ldots ,A_{n}\rightarrow$ $\højre pil$ $A,\Gamma$ $\Gamma ,A$ $\Gamma$ $EN$ $EN$

Aksiomer er begyndelsessekvenser, der accepteres uden bevis; i den sekventielle tilgang er antallet af aksiomer minimeret, så i Gentzens calculus er der kun givet ét skema af aksiomer - . Inferensregler i sekventiel form skrives som følgende udtryk: $\mathrm {LK}$ $\mathrm {LJ}$ $A\rightarrow A$

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

og ,

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

de tolkes som et udsagn om deducerbarheden fra den øvre sekvent (øvre sekvenser og ) af den nedre sekvent . Bevis i sekventiel beregning (som i systemer med naturlig inferens) er skrevet i træform fra top til bund, for eksempel: $S_{1}$ $S_{1}$ $S_{2}$ $T$

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

hvor hver linje betyder en direkte slutning - en overgang fra de øvre sekvenser til de nederste i henhold til en hvilken som helst af de slutningsregler, der er vedtaget i det givne system. Eksistensen af et inferenstræ, der starter fra aksiomer (initielle sekvenser) og fører til en sekvens , betyder dets udledningsevne i et givet logisk system: . $S$ $\vDash S$

Klassisk Gentzen sekvensregning

Den mest almindeligt anvendte sekvensregning til den klassiske prædikatregning er systemet konstrueret af Gentzen i 1934. Systemet har ét skema af aksiomer - og 21 slutningsregler, som er opdelt i strukturelle og logiske [11] . $\mathbf {LK}$ $A\rightarrow A$

Strukturelle regler (, — formler,,,, — lister over formler): $EN$ $B$ $\Gamma$ $\Delta$ $\Theta$ $\lambda$

dæmpning venstre: og højre: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A))$
forkortelse til venstre: og til højre: ; ${\cfrac {\,\,A,\ A,\ \Gamma \ \rightarrow \ \Delta }{\qquad A,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \Delta ,\ A\qquad ))$
permutation venstre: og højre: , ${\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 \ } }$
afsnit :. _ ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ Lambda }}$

Logiske propositionelle regler er designet til at tilføje propositionelle forbindelser til outputtet :

$\likke$ -venstre: ; -højre: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad ))$ $\likke$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ ))$
$\jord$ -venstre: og ; -højre: , ${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ $\jord$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$
$\lor$ -venstre: ; -højre : og $\ {\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øjre pil$ -venstre: og -højre :. $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$ $\Højre pil$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ A\Rightarrow B\ ))$

Logiske kvantificeringsregler introducerer universalitet og eksistenskvantatorer i afledningen ( er en formel med en fri variabel , er et vilkårligt udtryk og erstatter alle forekomster af en fri variabel med et led ): $F(a)$ $-en$ $t$ $F(t)$ $-en$ $t$

$\for alle$ -venstre: og -højre: ; ${\cfrac {\qquad F(t),\ \Gamma \ \rightarrow \ \Delta }{\ \forall x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\for alle$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \forall x:F(x)))$
$\eksisterer$ -venstre: og -højre :. ${\cfrac {\qquad F(a),\ \Gamma \ \rightarrow \ \Delta }{\ \exists x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\eksisterer$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(t)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \exists x:F(x)))$

En yderligere betingelse i kvantificeringsreglerne er manglende forekomst af en fri variabel i de nederste sekventielle formler i -højre og -venstre reglerne. $-en$ $\for alle$ $\eksisterer$

Et eksempel på udledningen af loven om den udelukkede midterste : $\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 begynder afledningen med et enkelt aksiom, derefter - reglerne - højre, - højre, permutation til højre, - højre og reduktion til højre anvendes successivt. $\likke$ $\lor$ $\lor$

Kalkulus svarer til den klassiske prædikatregning i første trin: en formel er gyldig i prædikatregningen, hvis og kun hvis sekventen kan udledes i . Nøgleresultatet , som Gentzen kaldte " hovedsætningen " ( tysk Hauptsatz ) er evnen til at udføre enhver slutning uden at anvende cut-reglen, det er takket være denne egenskab, at alle de grundlæggende egenskaber er etableret , inklusive korrekthed , konsistens og fuldstændighed. $\mathbf {LK}$ $EN$ $\mathbf {LK}$ $\rightarrow A$ $\mathbf {LK}$ $\mathbf {LK}$

Gentzens intuitionistiske sekvensregning

Regnestykket opnås ved at tilføje en begrænsning på sekvensernes succession i inferensreglerne: kun én formel er tilladt i dem, og reglerne for ret-permutation og ret-reduktion (der fungerer med flere formler i successive) er udelukket. Med minimale modifikationer opnås således et system, hvor lovene om dobbeltnegation og den udelukkede tredjedel ikke kan udledes , men alle andre grundlæggende logiske love gælder, og for eksempel ækvivalens kan udledes . Det resulterende system svarer til den intuitionistiske prædikatregning med Heytings aksiomatik . Sektioner kan også fjernes i calculus , den er også korrekt, konsistent og fuldstændig, desuden blev det sidste resultat for den intuitionistiske prædikatregning først opnået netop for . $\mathbf {LJ}$ $\mathbf {LK}$ $\lnot \lnot \lnot A\Leftrightarrow \lnot A$ $\mathbf {LJ}$ $\mathbf {LJ}$

Ikke-standard sekvensberegninger

Et stort antal ækvivalente og bekvemme varianter af sekventiel beregning for klassiske og intuitionistiske logikker er blevet skabt. Nogle af disse beregninger arver Gentzen-konstruktionen, der blev brugt til at bevise konsistensen af Peano-aritmetik og inkluderer elementer af systemer med naturlig afledning, blandt dem Sapps -systemet ( Patrick Suppes ; 1922-2014) fra 1957 [12] (taget fra Feis ' bemærkninger og Ladrière til den franske oversættelse af Gentzens papir) og dens forbedrede version udgivet i 1965 af John Lemmon ( 1930-1966 ) [13] , hvilket eliminerer den praktiske ulejlighed ved at bruge Gentzens originale Nutral Sequential [14] . Mere radikale forbedringer for den praktiske bekvemmelighed af naturtypeslutning i sekventielle beregninger blev foreslået af Hermes ( tysk: Hans Hermes ; 1912-2003) [15] : i hans system for klassisk logik anvendes to aksiomer ( og , og i reglerne af inferens bruges propositionelle bindeord ikke kun i efterfølgere, men også i antecedenter, desuden både i den nedre og i de øvre sekvenser [16] . $A\rightarrow A$ $\rightarrow A=A$

Symmetri

Sekventiel beregning er iboende i symmetri, der naturligt udtrykker dualitet , i aksiomatiske teorier formuleret af de Morgans love .

Noter

↑ Hertz P. Über Axiomensysteme für beliebige Satzsysteme (tysk) // Mathematische Annalen. - 1929. - Bd. 101 . - S. 457-514 . - doi : 10.1007/BF01454856 .
↑ Indrzejczak, 2014 , Hertz præsenterede ikke noget specifikt system for konkret logik. Hans tilgang var abstrakt; han definerede snarere et skema over systemet, hvor de eneste regler har en rent strukturel karakter, s. 1310.
↑ Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (tysk) // Mathematische Annalen. - 1932. - Bd. 107 . — S. 329–350 . - doi : 10.1007/BF01448897 .
↑ 1 2 Jan von Plateau, 2008 .
↑ Bernays P. Anmeldelse: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (engelsk) // Journal of Symbolic Logic . - 1945. - Bd. 10 , nej. 4 . - S. 127-130 .
↑ Suszko R. Formalna teoria wartości logicznych (polsk) // Studia Logica. - 1957. - T. 6 . — S. 145–320 .
↑ Indrzejczak, 2014 , 1310-1315, s. 1310.
↑ Kleene, 1958 , s. 389-406.
↑ Kleene, 1958 , s. 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 til logik. Princeton: Van Nostrand, 1957.
↑ Lemmon EJ Begyndende Logik. — London: Nelson, 1965.
↑ Indrzejczak, 2014 , s. 1300.
↑ Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
↑ Indrzejczak, 2014 , <...> For at opnå et mere fleksibelt værktøj til egentlig bevissøgning kan man indrømme muligheden for at lave logiske operationer også i forled. <…> Det lader til, at det første system af denne slags blev leveret af Hermes. Han bruger også intuitionistiske sekvenser med sekvenser af formler i antecedenter i sin formalisering af klassisk logik med identitet. Som primitive sekvenser bruger Hermes kun: og , s. 1300. $\varphi \Rightarrow \varphi$ $\Rightarrow \tau =\tau$

Litteratur

Sekvensregning // Safflower - Soan. - M .: Soviet Encyclopedia, 1976. - S. 181-182; Kunst. 530-532. - ( Great Soviet Encyclopedia : [i 30 bind] / chefredaktør A. M. Prokhorov ; 1969-1978, v. 23).
Dragalin A. G. Rækkefølgeregning // Mathematical Encyclopedia : [i 5 bind] / Kap. udg. I. M. Vinogradov . - M . : Soviet Encyclopedia, 1984. - T. 4: Ok - Slo. - S. 1104. - 1216 stb. : syg. — 150.000 eksemplarer.
Bystrov P.I. Sequence Calculus // New Philosophical Encyclopedia / Institute of Philosophy RAS ; national samfundsvidenskabeligt fond; Forrige. videnskabelig udg. råd V. S. Stepin , næstformænd: A. A. Guseynov , G. Yu. Semigin , revisor. hemmelighed A. P. Ogurtsov . — 2. udg., rettet. og tilføje. - 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 / oversat af A. V. Idelson. - M . : Nauka, 1967. - S. 9-76 .
Dragalin A. G. Matematisk intuitionisme. Introduktion til bevisteori. — M .: Nauka , 1979. — 256 s. — (Matematisk logik og matematikkens grundlag).
Kleene S. Introduction to Metamathematics / oversættelse fra engelsk af A. S. Yesenin-Volpin , redigeret af V. A. Uspensky . - M. : IL, 1958. - 527 s.
Takeuchi G. Bevisteori. - M . : Mir, 1978. - 412 s.
Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica . - 2014. - December ( bd. 102 , nr. 6 ). - S. 1295-1322 . - doi : 10.1007/s11225-014-9567-y .
Jan von Platon. Udviklingen af bevisteori . Stanford Encyclopaedia of Philosophy (16. april 2008). (ubestemt)

Logik

Filosofi • Semantik • Syntaks • Historie

Logiske grupper

klassisk logik	Aristotelisk logik propositionel logik Første ordens logik Anden ordens logik højere ordens logik
matematisk logik	mængdeteori Modelteori Beregnelighedsteori Bevisteori og konstruktiv matematik Lineær logik formelt system naturlig konklusion Sekvensberegning Algebra af logik Relevant logik Deontisk logik intuitionistisk logik Lambek regning
Ikke-klassisk logik	intuitionisme sløret logik Substrukturel logik logik Beskrivelseslogik Flerværdilogik Logisk syntese Bindende logik Tidsmæssig logik Modal logik ( Hybrid logik ) epistemisk logik
Filosofisk logik	Kritisk tænkning uformel logik deduktiv ræsonnement

Komponenter

Bortførelse (logik)
Sandsynlighed
udmelding
Fradrag / Induktion / Traduktion
Virkelighed
Induktiv begrundelse
slutning
boolsk konstant
Rigtigt
logisk følge
Logisk form
Nødvendige og tilstrækkelige betingelser
Beskrivelse
Definition
Substitution
Pakke
Kontrovers ( Antinomy )
Syntetisk dømmekraft / Analytisk dømmekraft
Link

Liste over booleske symboler