Takeuchiho domněnka je tvrzením o odstranitelnosti úseků v následném kalkulu pro jednoduchou teorii typů zkonstruovanou Gaishi Takeuchi (竹内外 史; 1926–2017) v roce 1953 [1] . Metodologický význam domněnky spočíval v tom, že odstranitelnost řezů pro tento kalkul otevírá cestu k důkazům správnosti , konzistence a úplnosti pro širokou třídu logiky vyššího řádu , analogicky s Gentzenovým výsledkem z roku 1934 pro klasický a intuicionistický první- řádový predikát kalkul .
Prvním krokem k potvrzení domněnky byl Taitův důkaz ( eng. William W. Tait ; nar. 1929) o odstranitelnosti sekcí v logice druhého řádu v roce 1966 [2] . V roce 1967 byl výsledek zobecněn v dílech Takahashiho [3] a Prawitze ( Swed. Dag Prawitz ; nar. 1936), čímž byla hypotéza zcela potvrzena.
Později byla objevena odnímatelnost sekcí pro širší třídy kalkulu, konkrétně Dragalin zavedl odstranitelnost sekcí pro řadu neklasických logik vyšších řádů a Girard ( fr. Jean-Yves Girard ) - pro systém F .