Aftagelighed af sektioner

Fjernbarhed af sektioner ( Gentzens sætning , eliminationssætning ) er en egenskab ved logiske calculi, ifølge hvilken enhver sekventiel deducibel i en given calculus kan udledes uden at anvende sektionsreglen [1] . Det spiller en grundlæggende rolle i bevisteori og en vigtig metodisk rolle i matematisk logik generelt på grund af det faktum, at det giver en konstruktiv metode til at bevise konsistens , især for klassiske og intuitionistiske logikker af første orden [2] .

For de klassiske og intuitionistiske sekvensregninger blev egenskaben bevist af Gentzen i 1934 . I 1953 blev Takeuchis formodning udtalt , ifølge hvilken fjernelse af sektioner finder sted for den simple teori om typer og de dertil svarende logikker af højere orden, senere blev det bekræftet - for den klassiske logik af anden orden, fjerneligheden af sektionerne blev bevist af Tate , for den simple teori om typer - Takahashi og Pravitsa , blev der hurtigt fundet beviser for en række ikke-klassiske højere ordensteorier ( Dragalin ) og avancerede typeteorier ( Girard for system F ).

Symbolsk formulering: lad og vær bevisbare sekvenser af calculus ; hvis er en calculus-sekvent , så er den beviselig [3] . $\Gamma \vdash \Theta ,\Phi$ $\Phi ,\Lambda \vdash \Delta$ $G$ $\Gamma ,\Lambda \vdash \Delta ,\Theta$ $G$

Noter

↑ Proof Theory, 1978 , s. 29.
↑ P. I. Bystrov. Eliminationssætning // New Philosophical Encyclopedia : i 4 bind / prev. videnskabeligt udg. råd fra V. S. Stepin . — 2. udg., rettet. og yderligere - M . : Tanke , 2010. - 2816 s.
↑ Ershov, 1987 , s. 214.

Litteratur

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