A szakaszok eltávolíthatósága

A szakaszok eltávolíthatósága ( Gentzen-tétel , eliminációs tétel ) a logikai számítások olyan tulajdonsága, amely szerint egy adott számításban bármely szekvenciális levezethető a szakaszszabály alkalmazása nélkül [1] . Alapvető szerepet játszik a bizonyítási elméletben , és általában véve fontos módszertani szerepet a matematikai logikában , mivel konstruktív módszert biztosít a konzisztencia bizonyítására , különösen az elsőrendű klasszikus és intuicionista logikákra [2] .

A klasszikus és intuíciós szekvenciális számításokhoz a tulajdonságot Gentzen bizonyította 1934 - ben . 1953- ban hangzott el Takeuchi sejtése , miszerint a szakaszok eltávolíthatósága az egyszerű típuselmélet és az ennek megfelelő magasabb rendű logikák esetében megtörténik, később beigazolódott - a másodrendű klasszikus logikára, az eltávolíthatóságra. a szakaszokat Tate bizonyította , az egyszerű típuselméletre - Takahashi és Pravitsa , hamarosan bizonyítékokat találtak egy sor nem klasszikus magasabb rendű elméletre ( Dragalin ) és fejlett típuselméletekre ( Girard az F rendszerhez ).

Szimbolikus megfogalmazás: legyen és legyen a kalkulus bizonyítható szekvenciája ; ha egy számítási szekvencia , akkor bizonyítható [3] . $\Gamma \vdash \Theta ,\Phi$ $\Phi ,\Lambda \vdash \Delta$ $G$ $\Gamma ,\Lambda \vdash \Delta ,\Theta$ $G$

Jegyzetek

↑ Bizonyításelmélet, 1978 , p. 29.
↑ P. I. Bystrov. Eliminációs tétel // Új Filozófiai Enciklopédia : 4 kötetben / előz. tudományos-szerk. V. S. Stepin tanácsa . — 2. kiadás, javítva. és további - M . : Gondolat , 2010. - 2816 p.
↑ Ershov, 1987 , p. 214.

Irodalom

G. Gentzen. Untersuchungen über das logische Schließen (német) // Mathematische Zeitschrift. – 1934–1935. — bd. 39 . – S. 405–431 . - doi : 10.1007/BF01201363 .
Takeuchi G. Bizonyításelmélet. - M . : Mir, 1978. - 412 p.
Ershov Yu. L. , Paljutyin E. A. Matematikai logika. — M .: Nauka, 1987. — 336 p.