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