Demontabilitatea secțiunilor

Demontabilitatea secțiunilor ( teorema lui Gentzen , teorema eliminării ) este o proprietate a calculului logic, conform căreia orice succesiune deductibilă într-un calcul dat poate fi dedusă fără a se aplica regula secțiunii [1] . Joacă un rol fundamental în teoria demonstrației și un rol metodologic important în logica matematică în general datorită faptului că oferă o metodă constructivă de demonstrare a consistenței , în special, pentru logica clasică și intuiționistă de ordinul întâi [2] .

Pentru calculele secvente clasice și intuiționiste , proprietatea a fost dovedită de Gentzen în 1934 . În 1953, s- a afirmat conjectura lui Takeuchi , conform căreia amovibilitatea secțiunilor are loc pentru teoria simplă a tipurilor și logica de ordin superior corespunzătoare acesteia, ulterior a fost confirmată - pentru logica clasică de ordinul doi, amovibilitatea secțiunile au fost dovedite de Tate , pentru teoria simplă a tipurilor - Takahashi și Pravitsa , în curând s-au găsit dovezi pentru o serie de teorii neclasice de ordin superior ( Dragalin ) și teorii avansate ale tipurilor ( Girard pentru sistemul F ).

Formulare simbolică: fie și fie secvențe demonstrabile ale calculului ; dacă este o secvență de calcul , atunci este demonstrabilă [3] . $\Gamma \vdash \Theta ,\Phi$ $\Phi ,\Lambda \vdash \Delta$ $G$ $\Gamma ,\Lambda \vdash \Delta ,\Theta$ $G$

Note

↑ Teoria dovezilor, 1978 , p. 29.
↑ P. I. Bystrov. Teorema eliminării // New Philosophical Encyclopedia : în 4 volume / prev. științific-ed. sfatul lui V. S. Stepin . — Ed. a II-a, corectată. si suplimentare - M . : Gândirea , 2010. - 2816 p.
↑ Ershov, 1987 , p. 214.

Literatură

G. Gentzen. Untersuchungen über das logische Schließen (germană) // Mathematische Zeitschrift. — 1934–1935. — bd. 39 . — S. 405–431 . - doi : 10.1007/BF01201363 .
Takeuchi G. Teoria dovezilor. - M . : Mir, 1978. - 412 p.
Ershov Yu. L. , Paliutin E. A. Logica matematică. — M .: Nauka, 1987. — 336 p.