Calcul de secvență

Calculul secvențelor este o variantă a calculului logic care folosește nu lanțuri arbitrare de tautologii pentru a demonstra enunțuri , ci secvențe de propoziții condiționate - secvențe . Cele mai cunoscute calcule secvențiale - și pentru calculul predicat clasic și intuiționist - au fost construite de Gentzen în 1934 , variantele secvențiale ulterioare au fost formulate pentru o clasă largă de calcule aplicate (aritmetică, analiză), teorii de tip, non -logici clasice. $\mathbf {LK}$ $\mathbf {LJ}$

În abordarea secvenţială, în loc de seturi largi de axiome , sunt utilizate sisteme dezvoltate de reguli de inferenţă , iar demonstraţia este realizată sub forma unui arbore de inferenţă; pe această bază (împreună cu sistemele de inferență naturală ), calculii secvenți sunt de tip Gentzen , spre deosebire de calculii axiomatici Hilbert , în care, cu un set dezvoltat de axiome, numărul de reguli de inferență se reduce la un minim.

Proprietatea principală a formei secvenţiale este dispozitivul simetric , care oferă comoditatea de a dovedi amovibilitatea secţiunilor , iar, ca urmare, calculii secvenţiali sunt principalele sisteme studiate în teoria demonstraţiei .

Istorie

Conceptul de secvent pentru utilizare sistematică în dovezi sub forma unui arbore de derivare a fost introdus în 1929 de către fizicianul și logicianul german Paul Hertz ( germană: Paul Hertz ; 1881-1940) [1] , dar un calcul holistic pentru orice logic teoria nu a fost construită în lucrările sale [2] . În lucrarea din 1932, Gentzen a încercat să dezvolte abordarea lui Hertz [3] , dar în 1934 a abandonat dezvoltările lui Hertz: a introdus sisteme de inferență naturale atât pentru calculul predicat clasic, cât și, respectiv, intuiționist, folosind tautologii obișnuite și arbori de inferență și, după cum dezvoltarea lor structurală, — sisteme secvențiale și . Căci și Gentzen au dovedit demontabilitatea tăieturii, ceea ce a dat un impuls metodologic semnificativ teoriei demonstrației evidențiate de Hilbert: în aceeași lucrare, Gentzen a dovedit mai întâi completitudinea calculului predicat intuiționist, iar în 1936 a dovedit consistența lui Peano. axiomatică pentru numere întregi, extinzându-l cu ajutorul unei variante secvențiale prin inducție transfinită la ordinal . Ultimul rezultat a avut și o semnificație ideologică specială în lumina pesimismului de la începutul anilor 1930 în legătură cu teorema de incompletitudine a lui Gödel , conform căreia consistența aritmeticii nu poate fi stabilită prin mijloace proprii: o extensie suficient de naturală a aritmeticii prin logică a fost a constatat că elimină această limitare. $\mathbf {NK}$ $\mathbf {NJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {NK}$ $\epsilon_0$

Următorul pas semnificativ în dezvoltarea calculului secvenţial a fost dezvoltarea în 1944 de către Oiva Ketonen ( fin. Oiva Ketonen ; 1913-2000) a unui calcul pentru logica clasică, în care toate regulile de inferenţă sunt reversibile; în același timp, Ketonen a propus o abordare de descompunere pentru a găsi dovezi folosind proprietatea de reversibilitate [4] [5] . Calculul fără axiome publicat în 1949 în disertația lui Roman Sushko era apropiat ca formă de construcțiile lui Hertz, fiind prima încarnare pentru sistemele secvențiale de tip hertzian [6] [7] .

În 1952, Stephen Kleene , în Introducerea în metamatematică, bazat pe calculul Ketonen, a construit un calcul secvenţial intuiţionist cu reguli de inferenţă reversibile [8] , a introdus şi calculul de tip Gentzen şi , care nu necesita inferenţa structurală reguli [9] , și , în general, după publicarea cărții, calculul secvent a devenit cunoscut într-un cerc larg de specialiști [4] . $G3i$ $G3c$

Începând cu anii 1950, atenția principală a fost acordată extinderii rezultatelor privind consistența și completitudinea la calculele predicate de ordin superior, teoria tipurilor , logicii non-clasice . În 1953, Gaishi Takeuchi (竹内外史; 1926–2017) a construit un calcul succesiv pentru o teorie simplă a tipurilor care exprimă calcule predicate de ordin superior și a sugerat că tăieturile sunt detașabile pentru aceasta ( conjectura lui Takeuchi ). În 1966, William Tate ( n. 1929 ) a dovedit capacitatea de îndepărtare a secțiunilor pentru logica de ordinul doi , în curând conjectura a fost pe deplin dovedită în lucrările lui Motoo Takahashi [10] și Dag Prawitz ( swed. Dag Prawitz ; n. 1936). În anii 1970, rezultatele au fost extinse semnificativ: Dragalin a găsit dovezi ale amovibilității secțiunilor pentru o serie de logici neclasice de ordin superior, iar Girard pentru sistemul F .

Începând cu anii 1980, sistemele secvenţiale au jucat un rol cheie în dezvoltarea sistemelor de demonstrare automată , în special, calculul secvenţial al construcţiilor dezvoltat de Thierry Cocan şi Gerard Huet în 1986 este un λ-calcul polimorf de ordin superior cu tipuri dependente care ocupă cel mai înalt punct din cubul λ Barendregt - folosit ca bază a sistemului software Coq .

Concepte de bază

Un succesiv este o expresie de forma, undeși sunt secvențe finite (posibil goale) de formule logice, numite: - antecedent , și - succesent ( uneori - consecvent ). Semnificația intuitivă stabilită în secvență este că dacă se realizează conjuncția formulelor antecedenteare loc (este derivată) disjuncția formulelor succesente. Uneori, în locul unei săgeți în notația unei secvențe, se folosește semnul de derivabilitate () sau semnul de implicație (). $\Gamma \rightarrow \Delta$ $\Gamma$ $\Delta$ $\Gamma$ $\Delta$ $A_{1},\ldots,A_{n}\rightarrow B_{1},\ldots,B_{m)$ $A_{1}\land \ldots \land A_{n)$ $B_{1}\lor \ldots \lor B_{m)$ $\Gamma \vdash \Delta$ $\Gamma \Rightarrow \Delta$

Dacă antecedentul este gol ( ), atunci este implicată disjuncția formulelor succesente ; un succesent gol ( ) este interpretat ca o inconsecvență în conjuncția formulelor antecedente. O secvență goală înseamnă că există o contradicție în sistemul luat în considerare. Ordinea formulelor în cedanți nu este semnificativă, dar numărul de apariții a unei instanțe de formulă într-un cedant contează. Înregistrarea în cesionari în forma sau , unde este o secvență de formule și este o formulă, înseamnă adăugarea unei formule la cesionar (poate într-o singură copie). $\rightarrow B_{1},\ldots, B_{m)$ $B_{1}\lor \ldots \lor B_{m)$ $A_{1},\ldots, A_{n}\rightarrow$ $\sageata dreapta$ $A,\Gamma$ $\Gamma ,A$ $\Gamma$ $A$ $A$

Axiomele sunt secvențe inițiale acceptate fără dovezi; în abordarea secvenţială, numărul de axiome este minimizat, deci, în calculul lui Gentzen , este dată o singură schemă de axiome - . Regulile de inferență în formă secvențială sunt scrise ca următoarele expresii: $\mathrm {LK}$ $\mathrm {LJ}$ $A\rightarrow A$

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

și ,

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

ele sunt interpretate ca o afirmație despre deductibilitatea din secvența superioară (secvențele superioare și ) ale secvenței inferioare . Dovada în calculul secvenţial (ca în sistemele de inferenţă naturală) este scrisă sub formă de arbore de sus în jos, de exemplu: $S_{1}$ $S_{1}$ $S_{2}$ $T$

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

unde fiecare linie înseamnă o inferență directă - o tranziție de la secvențele superioare la cele inferioare conform oricăreia dintre regulile de inferență adoptate în sistemul dat. Astfel, existența unui arbore de inferență care pleacă de la axiome (secvente inițiale) și care duce la o secvență înseamnă derivabilitatea acestuia într-un sistem logic dat: . $S$ $\vDash S$

Calcul secvent Gentzen clasic

Cel mai frecvent utilizat calcul secvenţial pentru calculul predicat clasic este sistemul construit de Gentzen în 1934. Sistemul are o schemă de axiome - și 21 de reguli de inferență, care sunt împărțite în structurale și logice [11] . $\mathbf {LK}$ $A\rightarrow A$

Reguli structurale (, — formule,,,, — liste de formule): $A$ $B$ $\Gamma$ $\Delta$ $\Theta$ $\lambda$

atenuare stânga: și dreapta: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A))$
abreviere în stânga: iar în dreapta: ; ${\cfrac {\,\,A,\A,\\Gamma \\rightarrow \\Delta }{\qquad A,\\Gamma \\rightarrow \\Delta \ ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \Delta ,\ A\qquad ))$
permutare stânga: și dreapta: , ${\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 \ } }$
sectiunea : . ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\\ Lambda }}$

Regulile propoziționale logice sunt concepute pentru a adăuga conexiuni propoziționale la rezultat :

$\lnu$ -stânga: ; -dreapta: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnu A,\ \Gamma \ \rightarrow \ \Delta \qquad ))$ $\lnu$ ${\cfrac {A,\ \Gamma \ \rightarrow \\Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ ))$
$\teren$ -stânga: și ; -dreapta :, ${\cfrac {\qquad A,\\Gamma \\rightarrow \\Delta }{\A\land B,\\Gamma \\rightarrow \\Delta \ ))$ ${\cfrac {\qquad B,\\Gamma \\rightarrow \\Delta }{\A\land B,\\Gamma \\rightarrow \\Delta \ ))$ $\teren$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$
$\lor$ -stânga: ; - dreapta : si $\ {\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\ ))$
$\Sageata dreapta$ -stânga: și -dreapta: . $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\\Gamma ,\\Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$ $\Sageata dreapta$ ${\cfrac {A,\\Gamma \\rightarrow \\Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \\Delta ,\ A\Rightarrow B\ ))$

Regulile cuantificatorilor logici introduc cuantificatori de universalitate și existență în derivare ( este o formulă cu o variabilă liberă , este un termen arbitrar și este înlocuirea tuturor aparițiilor unei variabile libere cu un termen ): $F(a)$ $A$ $t$ $F(t)$ $A$ $t$

$\pentru toți$ -stânga: și -dreapta: ; ${\cfrac {\qquad F(t),\\Gamma \\rightarrow \\Delta }{\\forall x:F(x),\\Gamma \\rightarrow \\Delta \ ))$ $\pentru toți$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\\Gamma \\rightarrow \\Delta ,\\forall x:F(x)))$
$\există$ -stânga: și -dreapta: . ${\cfrac {\qquad F(a),\\Gamma \\rightarrow \\Delta }{\\exists x:F(x),\\Gamma \\rightarrow \\Delta \ ))$ $\există$ ${\cfrac {\Gamma \ \rightarrow \ \Delta,\ F(t)\qquad }{\\Gamma \\rightarrow \\Delta,\\exists x:F(x)))$

O condiție suplimentară în regulile cuantificatorului este neapariția unei variabile libere în formulele secvențe inferioare din regulile -dreapta și -stânga. $A$ $\pentru toți$ $\există$

Un exemplu de derivare a legii mijlocului exclus : $\mathbf {LK}$

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

- în ea, derivarea începe cu o singură axiomă, apoi - se aplică succesiv regulile -dreapta, -dreapta, permutarea la dreapta, -dreapta și reducerea la dreapta. $\lnu$ $\lor$ $\lor$

Calculul este echivalent cu calculul predicat clasic din prima etapă: o formulă este valabilă în calculul predicat dacă și numai dacă secvența este derivabilă în . Rezultatul cheie, pe care Gentzen l-a numit „ teorema principală ” ( germană Hauptsatz ) este capacitatea de a efectua orice inferență fără a aplica regula de tăiere, datorită acestei proprietăți sunt stabilite toate proprietățile de bază , inclusiv corectitudinea , consistența și completitudine. $\mathbf {LK}$ $A$ $\mathbf {LK}$ $\rightarrow A$ $\mathbf {LK}$ $\mathbf {LK}$

Calculul secvențial intuiționist al lui Gentzen

Calculul se obține prin adăugarea unei restricții asupra succesentelor secvenților în regulile de inferență: în ele este permisă o singură formulă, iar regulile de permutare dreaptă și de reducere dreaptă (operând cu mai multe formule în succesenți) sunt excluse. Astfel, cu modificări minime, se obține un sistem în care legile dublei negații și treimea exclusă nu sunt derivabile , dar se aplică toate celelalte legi logice de bază și, de exemplu, echivalența este derivabilă . Sistemul rezultat este echivalent cu calculul predicat intuiționist cu axiomatica lui Heyting . Secțiunile sunt și ele detașabile în calcul , este și corect, consistent și complet, în plus, ultimul rezultat pentru calculul predicat intuiționist a fost obținut pentru prima dată tocmai pentru . $\mathbf {LJ}$ $\mathbf {LK}$ $\lnu \lnu \lnu A\Leftrightarrow \lnot A$ $\mathbf {LJ}$ $\mathbf {LJ}$

Calcule succesive non-standard

S-au creat un număr mare de variante echivalente și convenabile ale calculului secvențial pentru logica clasică și intuiționistă. Unii dintre acești calculi moștenesc construcția Gentzen folosită pentru a demonstra consistența aritmeticii Peano și includ elemente ale sistemelor de derivație naturală, printre care sistemul Sapps ( Patrick Suppes ; 1922–2014) din 1957 [12] (preluat din observațiile lui Feis ). și Ladrière la traducerea în franceză a lucrării lui Gentzen) și versiunea sa îmbunătățită publicată în 1965 de John Lemmon ( 1930-1966 ) [13] , eliminând inconvenientul practic de a utiliza Sequentialul Nutral original al lui Gentzen [14] . Îmbunătățiri mai radicale pentru comoditatea practică a inferenței de tip natural în calculele secvențiale au fost propuse de Hermes ( germană: Hans Hermes ; 1912-2003) [15] : în sistemul său pentru logica clasică, sunt aplicate două axiome ( și , și în reguli ). de inferență, conectivele propoziționale sunt folosite nu numai în succesenți, ci și în antecedente, de altfel, atât în secvențele inferioare, cât și în cele superioare [16] . $A\rightarrow A$ $\rightarrow A=A$

Simetrie

Calculul secvenţial este inerent simetriei, exprimând în mod natural dualitatea , în teoriile axiomatice formulate de legile lui de Morgan .

Note

↑ Hertz P. Über Axiomensysteme für beliebige Satzsysteme (germană) // Mathematische Annalen. - 1929. - Bd. 101 . - S. 457-514 . - doi : 10.1007/BF01454856 .
↑ Indrzejczak, 2014 , Hertz nu a prezentat niciun sistem specific pentru logica concretă. Abordarea lui a fost abstractă; el a definit mai degrabă o schemă a sistemului în care singurele reguli au un caracter pur structural, p. 1310.
↑ Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (germană) // Mathematische Annalen. - 1932. - Bd. 107 . — S. 329–350 . - doi : 10.1007/BF01448897 .
↑ 1 2 Jan von Plateau, 2008 .
↑ Bernays P. Review: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (engleză) // Journal of Symbolic Logic . - 1945. - Vol. 10 , nr. 4 . - P. 127-130 .
↑ Suszko R. Formalna teoria wartości logicznych (poloneză) // Studia Logica. - 1957. - T. 6 . — S. 145–320 .
↑ Indrzejczak, 2014 , 1310-1315, p. 1310.
↑ Kleene, 1958 , p. 389-406.
↑ Kleene, 1958 , p. 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. Introducere în logică. Princeton: Van Nostrand, 1957.
↑ Lemmon EJ Începutul logicii. — Londra: Nelson, 1965.
↑ Indrzejczak, 2014 , p. 1300.
↑ Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
↑ Indrzejczak, 2014 , <...> pentru a obține un instrument mai flexibil pentru căutarea probelor efective se poate admite posibilitatea de a face operații logice și în antecedente. <…> Se pare că primul sistem de acest fel a fost oferit de Hermes. El folosește, de asemenea, secvențe intuiționiste cu secvențe de formule în antecedente în formalizarea sa a logicii clasice cu identitate. Ca secvențe primitive Hermes folosește numai: și , p. 1300. $\varphi \Rightarrow \varphi$ $\Rightarrow \tau =\tau$

Literatură

Calcul de secvență // Sofflower - Soan. - M .: Enciclopedia Sovietică, 1976. - S. 181-182; Artă. 530-532. - ( Marea Enciclopedie Sovietică : [în 30 de volume] / redactor-șef A. M. Prohorov ; 1969-1978, v. 23).
Dragalin A. G. Calcul de secvențe // Enciclopedia matematică : [în 5 volume] / Cap. ed. I. M. Vinogradov . - M . : Enciclopedia Sovietică, 1984. - T. 4: Ok - Slo. - S. 1104. - 1216 stb. : bolnav. — 150.000 de exemplare.
Bystrov P.I. Sequence Calculus // New Philosophical Encyclopedia / Institute of Philosophy RAS ; Naţional social-științifice fond; Prev. științific-ed. consiliul V. S. Stepin , vicepreședinți: A. A. Guseynov , G. Yu. Semigin , contabil. secret A. P. Ogurţov . — Ed. a II-a, corectată. si adauga. - M .: Gândirea , 2010. - ISBN 978-5-244-01115-9 .
Gentzen G. Studii de inferență = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Idelson A. V., Mints G. E. Teoria matematică a inferenței / tradus de A. V. Idelson. - M .: Nauka, 1967. - S. 9-76 .
Dragalin A. G. Intuiţionism matematic. Introducere în teoria dovezilor. — M .: Nauka , 1979. — 256 p. — (Logica matematică și fundamentele matematicii).
Kleene S. Introducere în metamatematică / traducere din engleză de A. S. Yesenin-Volpin , editată de V. A. Uspensky . - M. : IL, 1958. - 527 p.
Takeuchi G. Teoria dovezilor. - M . : Mir, 1978. - 412 p.
Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica . - 2014. - Decembrie ( vol. 102 , Nr. 6 ). - S. 1295-1322 . - doi : 10.1007/s11225-014-9567-y .
Jan von Plato. Dezvoltarea teoriei probei . Stanford Encyclopaedia of Philosophy (16 aprilie 2008). (nedefinit)

Logici

Filosofie • Semantică • Sintaxă • Istorie

Grupuri logice

logica clasica	logica aristotelică Logica propozițională Logica de ordinul întâi Logica de ordinul doi logica de ordin superior
logica matematica	teoria multimilor Teoria modelului Teoria computabilității Teoria dovezilor și matematică constructivă Logica liniară sistem formal concluzie firească Calcul de secvență Algebra logicii Logica relevanta Logica deontică logica intuiționistă calculul Lambek
Logica non-clasică	intuitionism logica fuzzy Logica substructurala logica Logica descrierii Logica cu mai multe valori Sinteza logica Logica obligatorie Logica temporală Logica modală ( logica hibridă ) logica epistemică
Logica filozofică	Gândire critică logica informala motiv dedus

Componente

Lista simbolurilor booleene