Sorozatszámítás

A szekvenciaszámítás a logikai számítás egyik változata , amely nem tetszőleges tautológiák láncait használja az állítások bizonyítására , hanem feltételes propozíciók sorozatait - szekvenciák . A leghíresebb szekvenciális számításokat - és a klasszikus és intuicionista predikátumszámításhoz - Gentzen építette 1934 -ben , későbbi szekvenciális változatokat fogalmaztak meg az alkalmazott kalkulusok (számtani, elemzési), típuselméletek, nem. - klasszikus logika. $\mathbf {LK}$ $\mathbf {LJ}$

A szekvenciális megközelítésben az axióma széles halmaza helyett fejlett következtetési szabályrendszereket használnak , és a bizonyítást egy következtetési fa formájában hajtják végre; ezen az alapon ( a természetes következtetési rendszerekkel együtt ) a szekvenciális számítások Gentzen típusúak , ellentétben az axiomatikus Hilbert -számítással , amelyben egy kidolgozott axiómakészlettel a következtetési szabályok száma egy minimális.

A szekvenciális forma fő tulajdonsága a szimmetrikus eszköz , amely a szakaszok kivehetőségének bizonyításának kényelmét biztosítja , és ennek eredményeként a szekvenciális kalkulusok a fő vizsgált rendszerek a bizonyításelméletben .

Történelem

A szekvencia fogalmát a bizonyításokban levezetési fa formájában történő szisztematikus használatára 1929 -ben Paul Hertz német fizikus és logikus vezette be ( németül: Paul Hertz ; 1881-1940) [1] , de holisztikus számítás minden logikára. az elmélet nem épült fel műveiben [2] . Gentzen 1932-es munkájában megpróbálta továbbfejleszteni a hertzi megközelítést [3] , de 1934-ben felhagyott a hertzi fejlesztésekkel: természetes következtetési rendszereket vezetett be mind a klasszikus, mind az intuíciós predikátumszámításhoz, közönséges tautológiák és következtetési fák segítségével, és mint pl. szerkezeti fejlődésük, — szekvenciális rendszerek és . For és Gentzen bebizonyította a vágás eltávolíthatóságát, ami jelentős módszertani lökést adott a Hilbert által felvázolt bizonyítási elméletnek: ugyanebben a művében Gentzen először bizonyította az intuicionista predikátumszámítás teljességét, majd 1936-ban bebizonyította a Peano-féle állítás konzisztenciáját . axiomatika egész számokra, egy szekvenciális változat segítségével, transzfinit indukcióval ordinálisra bővítve . Ez utóbbi eredménynek különös ideológiai jelentősége is volt a 30-as évek eleji pesszimizmus tükrében Gödel hiányossági tételével kapcsolatban , amely szerint az aritmetika konzisztenciája önmagában nem állapítható meg: az aritmetika logikailag kellően természetes kiterjesztése. megállapította, hogy ez megszünteti ezt a korlátozást. $\mathbf {NK}$ $\mathbf {NJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {LK}$ $\mathbf {LJ}$ $\mathbf {NK}$ $\epsilon_0$

A következő jelentős lépés a szekvenciális kalkulus fejlesztésében az volt, hogy Oiva Ketonen ( fin. Oiva Ketonen ; 1913-2000) 1944 -ben kifejlesztett egy klasszikus logikai kalkulust, amelyben minden következtetési szabály megfordítható; ugyanakkor Ketonen egy dekompozíciós megközelítést javasolt a bizonyítékok megtalálásához a visszafordíthatósági tulajdonság segítségével [4] [5] . A Roman Sushko disszertációjában 1949-ben publikált axiómamentes kalkulus formailag közel állt Hertz konstrukcióihoz, ez volt a hertzi típusú szekvenciális rendszerek első inkarnációja [6] [7] .

Stephen Kleene 1952 - ben a Bevezetés a metamatematikába című művében, a Ketonen-számítás alapján, intuicionista szekvenciaszámítást konstruált reverzibilis következtetési szabályokkal [8] , bevezette a Gentzen-típusú kalkulust és , amelyhez nem volt szükség strukturális következtetésre . szabályok [9] , és általában a könyv megjelenése után a szekvenciális kalkulus a szakemberek széles körében vált ismertté [4] . $G3i$ $G3c$

Az 1950-es évek óta a fő figyelem a konzisztenciára és teljességre vonatkozó eredmények kiterjesztésére irányul a magasabb rendű predikátumszámításokra, a típuselméletre , a nem klasszikus logikára . 1953- ban Gaishi Takeuchi (竹内外史; 1926–2017) megszerkesztett egy szekvenciális kalkulust egy egyszerű típuselmélethez, amely magasabb rendű predikátumkalculusokat fejez ki, és azt javasolta, hogy a vágások eltávolíthatók számára ( Takeuchi sejtése ). 1966- ban William Tate ( sz . 1929 ) bebizonyította a szakaszok eltávolíthatóságát a másodrendű logika számára, hamarosan Motoo Takahashi [10] és Dag Prawitz ( svéd Dag Prawitz ; sz. 1936) munkáiban teljes mértékben bebizonyosodott a sejtés . Az 1970-es években az eredmények jelentősen bővültek: Dragalin egy sor magasabb rendű nemklasszikus logika esetében talált bizonyítékot a szakaszok eltávolíthatóságára, míg Girard az F rendszerre .

Az 1980-as évek óta a szekvenciális rendszerek kulcsszerepet játszottak az automatikus bizonyítási rendszerek kifejlesztésében , különösen a Thierry Cocan és Gerard Huet által 1986-ban kifejlesztett szekvenciális konstrukciók számítása egy magasabb rendű polimorf λ-számítás függő típusokkal . a λ-kocka legmagasabb pontja a Barendregt - a Coq szoftverrendszer alapjaként .

Alapfogalmak

A szekvencia a forma kifejezése, aholés a logikai formulák véges (esetleg üres) sorozatai, amelyeket cedenseknek neveznek : - előzmény , és - utódlás (néha - konzekvens ). A szekvenciában lefektetett intuitív jelentés az , hogy haelőzményképletek konjunkcióját , akkor az egymást követő formulák diszjunkciója megtörténik (levezetve). Néha egy sorozat jelölésében nyíl helyett a származtatási jelet () vagy az implikációs jelet () használják. $\Gamma \jobbra \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$

Ha az előzmény üres ( ), akkor a következő képletek diszjunkcióját jelenti ; az üres utódot ( ) az előzményképletek összefüggésének inkonzisztenciájaként értelmezzük. Az üres szekvencia azt jelenti, hogy a vizsgált rendszerben ellentmondás van. A képletek sorrendje a cedantokban nem jelentős, de a képletpéldány előfordulások száma egy cedantban számít. A jelölőkben való rögzítés a vagy formában , ahol képletsorozat, és egy képlet, azt jelenti, hogy képletet adunk a hozzárendelőhöz (talán még egy példányban). ${\displaystyle \rightarrow B_{1},\ldots ,B_{m))$ ${\displaystyle B_{1}\lor \ldots \lor B_{m))$ $A_{1},\ldots ,A_{n}\rightarrow$ $\jobb nyíl$ $A,\Gamma$ $\Gamma ,A$ $\Gamma$ $A$ $A$

Az axiómák bizonyítás nélkül elfogadott kezdeti sorozatok; a szekvenciális megközelítésben az axiómák száma minimalizálva van, így a Gentzen-számításban csak egy axiómaséma adott - . A szekvenciális formájú következtetési szabályok a következő kifejezésekként vannak írva: $\mathrm {LK}$ $\mathrm {LJ}$ $A\rightarrow A$

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

és ,

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

az alsó szekvencia felső szekvenciájából (felső szekvenciák és ) levezethetőségére vonatkozó állításként értelmeződnek . A szekvenciális számításban (mint a természetes következtetési rendszerekben) a bizonyítást fa formában írják felülről lefelé, például: $S_{1}$ $S_{1}$ $S_{2}$ $T$

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

ahol minden sor közvetlen következtetést jelent - átmenetet a felső sorozatokból az alsókba az adott rendszerben elfogadott bármely következtetési szabály szerint. Így az axiómákból (kezdeti szekvenciákból) kiinduló és szekvenciához vezető következtetési fa létezése egy adott logikai rendszerben levezethetőségét jelenti: . $S$ $\vDash S$

Klasszikus Gentzen szekvenciális kalkulus

A klasszikus predikátumszámítás leggyakrabban használt szekvenciális számítása a Gentzen által 1934-ben felépített rendszer. A rendszer egy axióma sémával és 21 következtetési szabállyal rendelkezik, amelyek strukturális és logikai csoportokra oszlanak [11] . $\mathbf {LK}$ $A\rightarrow A$

Strukturális szabályok (, — képletek,,,, — képletlisták): $A$ $B$ $\Gamma$ $\Delta$ $\Theta$ $\lambda$

csillapítás balra: és jobbra: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A))$
rövidítés a bal oldalon: és a jobb oldalon: ; ${\cfrac {\,\,A,\ A,\ \Gamma \ \rightarrow \ \Delta }{\qquad A,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \Delta ,\ A\qquad ))$
permutáció balra: és jobbra: , ${\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 \ } }$
szakasz : . ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ Lambda }}$

A logikai propozíciós szabályok úgy vannak kialakítva, hogy propozíciós kapcsolatokat adjanak a kimenethez :

$\lnem$ -balra: ; -jobbra: ; ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad ))$ $\lnem$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ ))$
$\föld$ -balra: és ; -jobbra: , ${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ ${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ ))$ $\föld$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$
$\lor$ -balra: ; -jobbra : és $\ {\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\vagy B\ ))$ ${\cfrac {\Gamma \rightarrow \Delta ,\ B\qquad }{\ \Gamma \rightarrow \Delta ,\ A\lor B\ ))$
$\Jobb nyíl$ -bal: és -jobb : . $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \jobbra \ \Delta ,\Lambda \qquad }}$ $\Jobb nyíl$ ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ A\Rightarrow B\ ))$

A logikai kvantorszabályok univerzalitási és létezési kvantorokat vezetnek be a levezetésbe ( egy szabad változós képlet , egy tetszőleges tag, és egy szabad változó minden előfordulását helyettesíti egy taggal ): $F(a)$ $a$ $t$ $F(t)$ $a$ $t$

$\mindenkinek$ -bal: és -jobb : ; ${\cfrac {\qquad F(t),\ \Gamma \ \rightarrow \ \Delta }{\ \forall x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\mindenkinek$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \forall x:F(x)))$
$\létezik$ -bal: és -jobb : . ${\cfrac {\qquad F(a),\ \Gamma \ \rightarrow \ \Delta }{\ \exists x:F(x),\ \Gamma \ \rightarrow \ \Delta \ ))$ $\létezik$ ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(t)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \exists x:F(x)))$

A kvantorszabályok további feltétele, hogy a -jobb és -bal szabályban az alsó szekvenciális képletekben ne forduljon elő szabad változó . $a$ $\mindenkinek$ $\létezik$

Példa a kizárt középső törvény levezetésére : $\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\vagy \lnot A\quad }}{\quad \ \rightarrow \ A\vagy \lnot A}}

- benne a levezetés egyetlen axiómával kezdődik, majd - a -jobb, -jobb, jobb oldali permutáció, -jobb és redukció a jobb oldalon egymás után érvényesül. $\lnem$ $\lor$ $\lor$

A kalkulus ekvivalens az első szakasz klasszikus predikátumszámításával: egy formula akkor és csak akkor érvényes a predikátumszámításban, ha a szekvencia származtatható -ben . A legfontosabb eredmény, amelyet Gentzen „ főtételnek ” ( német Hauptsatz ) nevezett, az a képesség, hogy bármilyen következtetést lehessen levonni a vágási szabály alkalmazása nélkül, ennek a tulajdonságnak köszönhető, hogy minden alapvető tulajdonság létrejön , beleértve a helyességet , a konzisztenciát és teljesség. $\mathbf {LK}$ $A$ $\mathbf {LK}$ $\rightarrow A$ $\mathbf {LK}$ $\mathbf {LK}$

Gentzen intuicionista szekvenciális számítása

A számítást úgy kapjuk meg, hogy a következtetési szabályokban a szekvenciák utódaira vonatkozó korlátozást adunk: csak egy képlet megengedett bennük, és a jobb permutáció és a jobb redukció szabályai (a szekvenciákban több képlettel operálva) ki vannak zárva. Így minimális módosításokkal olyan rendszert kapunk, amelyben a kettős tagadás és a kizárt harmad törvényei nem származtathatók , de minden más alapvető logikai törvény érvényes, és például az ekvivalencia származtatható . Az eredményül kapott rendszer ekvivalens a Heyting-féle axiomatikájú intuíciós predikátumszámítással . A metszetek is eltávolíthatók a kalkulusban , ez is helyes, következetes és teljes, ráadásul az intuíciós predikátumszámítás utolsó eredményét először pontosan a -ra kaptuk . $\mathbf {LJ}$ $\mathbf {LK}$ $\lnot \lnot \lnot A\Leftrightarrow \lnot A$ $\mathbf {LJ}$ $\mathbf {LJ}$

Nem szabványos szekvenciális számítások

A klasszikus és intuicionista logikák szekvenciális számításának számos ekvivalens és kényelmes változatát hozták létre. Ezen számítások egy része a Peano aritmetika konzisztenciájának bizonyítására használt Gentzen-konstrukciót örökli, és természetes levezetési rendszerek elemeit tartalmazzák, köztük az 1957-es Sapps- rendszert ( Patrick Suppes ; 1922–2014) [12] ( Feis megjegyzéseiből átvéve). és Ladrière Gentzen dolgozatának francia fordításához) és annak továbbfejlesztett változatát, amelyet 1965-ben adott ki John Lemmon ( 1930-1966 ) [13] , kiküszöbölve a Gentzen eredeti Nutral Sequential [14] használatával járó gyakorlati kényelmetlenséget . A szekvenciális számítások természetes típuskövetkeztetésének gyakorlati kényelmére radikálisabb fejlesztéseket javasolt Hermes ( németül: Hans Hermes ; 1912-2003) [15] : a klasszikus logika rendszerében két axiómát alkalmaznak ( és , valamint a szabályokban A következtetéshez a propozíciós konnektívumokat nemcsak utódok, hanem előzmények is használják, sőt mind az alsó, mind a felső szekvenciákban [16] . $A\rightarrow A$ $\rightarrow A=A$

Szimmetria

A szekvenciális kalkulus a szimmetriában rejlik, és természetesen kifejezi a kettősséget , a de Morgan törvényei által megfogalmazott axiomatikus elméletekben .

Jegyzetek

↑ Hertz P. Über Axiomensysteme für beliebige Satzsysteme (német) // Mathematische Annalen. - 1929. - Bd. 101 . - S. 457-514 . - doi : 10.1007/BF01454856 .
↑ Indrzejczak, 2014 , a Hertz nem mutatott be konkrét logikai rendszert. Megközelítése elvont volt; inkább a rendszer sémáját határozta meg, amelyben az egyedüli szabályok tisztán strukturális jellegűek, p. 1310.
↑ Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (német) // Mathematische Annalen. - 1932. - Bd. 107 . – S. 329–350 . - doi : 10.1007/BF01448897 .
↑ 2008. január 1 2. von Plateau .
↑ Bernays P. Review: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (angol) // Journal of Symbolic Logic . - 1945. - 1. évf. 10 , sz. 4 . - 127-130 . o .
↑ Suszko R. Formalna teoria wartości logicznych (lengyel) // 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 vágás-eliminációs tétel bizonyítéka az egyszerű típuselméletben // Journal of Japanese Mathematical Society. - 1967. - T. 19 , 4. sz . - S. 399-410 . - doi : 10.2969/jmsj/01940399 .
↑ Takeuchi, 1978 .
↑ Suppes P. Bevezetés a logikába. Princeton: Van Nostrand, 1957.
↑ Lemmon EJ Beginning Logic. – London: Nelson, 1965.
↑ Indrzejczak, 2014 , p. 1300.
↑ Hermes H. Einführung in die Mathematische Logik. – Stuttgart: Teubner, 1963.
↑ Indrzejczak, 2014 , <...> a tényleges bizonyítási keresés rugalmasabb eszközének megszerzése érdekében az előzményekben is megengedhető a logikai műveletek elvégzésének lehetősége. <…> Úgy tűnik, hogy az első ilyen rendszert Hermész biztosította. A klasszikus logika identitással való formalizálásában is intuicionista szekvenciákat használ képletsorozatokkal az előzményekben. Primitív sorozatként Hermész csak a következőket használja: és , p. 1300. $\varphi \Rightarrow \varphi$ $\Rightarrow \tau =\tau$

Irodalom

Sorozatszámítás // Pórsáfrány - Soan. - M .: Szovjet Enciklopédia, 1976. - S. 181-182; Művészet. 530-532. - ( Nagy Szovjet Enciklopédia : [30 kötetben] / főszerkesztő A. M. Prohorov ; 1969-1978, 23. v.).
Dragalin A. G. Sorozatszámítás // Matematikai enciklopédia : [5 kötetben] / Ch. szerk. I. M. Vinogradov . - M . : Szovjet Enciklopédia, 1984. - T. 4: Ok - Slo. - S. 1104. - 1216 stb. : ill. — 150.000 példány.
Bystrov P.I. Sequence Calculus // New Philosophical Encyclopedia / Institute of Philosophy RAS ; Nemzeti társadalomtudományi alap; Előző tudományos-szerk. tanács V. S. Stepin , alelnökök: A. A. Guseynov , G. Yu. Semigin , könyvelő. titok A. P. Ogurcov . — 2. kiadás, javítva. és add hozzá. - M .: Gondolat , 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. A következtetés matematikai elmélete / A. V. Idelson fordítása. - M . : Nauka, 1967. - S. 9-76 .
Dragalin A. G. Matematikai intuíció. Bevezetés a bizonyításelméletbe. — M .: Nauka , 1979. — 256 p. — (Matematikai logika és a matematika alapjai).
Kleene S. Bevezetés a metamatematikába / fordítás angolból : A. S. Yesenin-Volpin , szerkesztette: V. A. Uspensky . - M. : IL, 1958. - 527 p.
Takeuchi G. Bizonyításelmélet. - M . : Mir, 1978. - 412 p.
Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica . - 2014. - December ( 102. évf. 6. szám ). - S. 1295-1322 . - doi : 10.1007/s11225-014-9567-y .
Jan von Platón. A bizonyítási elmélet fejlődése . Stanford Encyclopaedia of Philosophy (2008. április 16.). (határozatlan)

Logikák

Filozófia • Szemantika • Szintaxis • Történelem

Logikai csoportok

klasszikus logika	Arisztotelészi logika propozíciós logika Elsőrendű logika Másodrendű logika magasabb rendű logika
matematikai logika	halmazelmélet Modellelmélet Kiszámíthatóság elmélet Bizonyításelmélet és konstruktív matematika Lineáris logika formális rendszer természetes következtetés Sorozatszámítás Logikai algebra Releváns logika Deontikus logika intuicionista logika Lambek kalkulus
Nem klasszikus logika	intuicionizmus zavaros logika Szubstrukturális logika logika Leírás logika Többértékű logika Logikai szintézis Kötési logika Időbeli logika Modális logika ( Hibrid logika ) episztemikus logika
Filozófiai logika	Kritikus gondolkodás informális logika deduktív érvelés

Alkatrészek

Logikai szimbólumok listája