Osien irrotettavuus

Osien irrotettavuus ( Gentzenin lause , eliminaatiolause ) on loogisen laskun ominaisuus, jonka mukaan mikä tahansa peräkkäinen päätelmä tietyssä laskussa voidaan päätellä ilman leikkaussääntöä [1] . Sillä on perustavanlaatuinen rooli todistusteoriassa ja tärkeä metodologinen rooli matemaattisessa logiikassa yleensä, koska se tarjoaa rakentavan menetelmän johdonmukaisuuden todistamiseen , erityisesti klassisen ja intuitionistisen ensimmäisen asteen logiikan [2] .

Gentzen osoitti ominaisuuden klassisille ja intuitionistisille sekventiolaskuille vuonna 1934 . Vuonna 1953 esitettiin Takeuchin olettamus , jonka mukaan osien irrotettavuus tapahtuu yksinkertaiselle tyyppiteorialle ja sitä vastaavalle korkeamman asteen logiikalle, myöhemmin se vahvistettiin - toisen asteen klassiselle logiikalle, osien irrotettavuus. osien todisti Tate , yksinkertaiselle tyyppiteorialle - Takahashi ja Pravitsa , todisteet löydettiin pian sarjalle ei-klassisia korkeamman asteen teorioita ( Dragalin ) ja edistyneitä tyyppiteorioita ( Girard järjestelmälle F ).

Symbolinen muotoilu: Olkoon ja oltava todistettavissa olevia laskentajaksoja ; jos on laskentasekvenssi , niin se on todistettavissa [3] . $\Gamma \vdash \Theta ,\Phi$ $\Phi ,\Lambda \vdash \Delta$ $G$ $\Gamma ,\Lambda \vdash \Delta ,\Theta$ $G$

Muistiinpanot

↑ Todistusteoria, 1978 , s. 29.
↑ P. I. Bystrov. Eliminaatiolause // New Philosophical Encyclopedia : 4 osassa / esi. tieteellinen toim. V. S. Stepinin neuvo . — 2. painos, korjattu. ja ylimääräistä - M . : Ajatus , 2010. - 2816 s.
↑ Ershov, 1987 , s. 214.

Kirjallisuus

G. Gentzen. Untersuchungen über das logische Schließen (saksa) // Mathematische Zeitschrift. - 1934-1935. - bd. 39 . — S. 405–431 . - doi : 10.1007/BF01201363 .
Takeuchi G. Todistusteoria. - M .: Mir, 1978. - 412 s.
Ershov Yu. L. , Palyutin E. A. Matemaattinen logiikka. - M .: Nauka, 1987. - 336 s.