Takeuchis gissning är ett uttalande om borttagningsbarheten av sektioner i den efterföljande kalkylen för en enkel typteori konstruerad av Gaishi Takeuchi (竹内外 史; 1926–2017) 1953 [1] . Den metodologiska betydelsen av gissningen var att borttagningsförmågan av skärningar för denna kalkyl öppnar vägen för bevis på korrekthet , konsistens och fullständighet för en bred klass av logiker av högre ordning , i analogi med Gentzens resultat från 1934 för den klassiska och intuitionistiska första- ordningspredikatkalkyl . _
Det första steget mot bekräftelsen av gissningen var beviset av Tait ( eng. William W. Tait ; född 1929) på borttagningsbarheten av sektioner i andra ordningens logik 1966 [ 2] . År 1967 generaliserades resultatet i verk av Takahashi [3] och Prawitz ( Svenska Dag Prawitz ; född 1936), så hypotesen bekräftades helt.
Senare upptäcktes borttagbarheten av sektioner för bredare klasser av tandstenar, i synnerhet Dragalin etablerade borttagbarheten av sektioner för en serie icke-klassiska logiker av högre ordning, och Girard ( fr. Jean-Yves Girard ) - för systemet F .