Takeuchi sejtése egy állítás a szakaszok eltávolíthatóságáról a szekvenciális kalkulusban egy egyszerű típuselmélethez , amelyet Gaishi Takeuchi (竹内外 史; 1926–2017) konstruált meg 1953-ban [1] . A sejtés módszertani jelentősége az volt, hogy a vágások eltávolíthatósága ennél a számításnál megnyitja az utat a helyesség , a következetesség és a teljesség bizonyítása előtt a magasabb rendű logikák széles osztálya számára , Gentzen 1934-es, a klasszikus és intuicionista első- állítmányszámítási sorrend .
Az első lépés a sejtés megerősítése felé az volt, hogy Tait ( eng. William W. Tait ; született 1929-ben) 1966 - ban bebizonyította, hogy a szakaszok eltávolíthatók a másodrendű logikában [2] . 1967 -ben az eredményt Takahashi [3] és Prawitz ( svéd Dag Prawitz ; szül. 1936) munkáiban általánosították, így a hipotézis teljes mértékben beigazolódott.
Később felfedezték a metszetek eltávolíthatóságát a kalkulusok szélesebb osztályaihoz, különösen Dragalin egy sor nem klasszikus magasabb rendű logikához, Girard ( fr. Jean-Yves Girard ) pedig az F rendszerhez állapította meg a szakaszok eltávolíthatóságát. .