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] .