Takeuchis formodning er et udsagn om fjernelse af sektioner i den efterfølgende beregning for en simpel typeteori konstrueret af Gaishi Takeuchi (竹内外 史; 1926–2017) i 1953 [1] . Den metodiske betydning af formodningen var, at fjerneligheden af snit for denne kalkulus åbner vejen for beviser for korrekthed , konsistens og fuldstændighed for en bred klasse af højere-ordens logikker , analogt med Gentzens resultat fra 1934 for den klassiske og intuitionistiske første- rækkefølge prædikat calculi .
Det første skridt i retning af bekræftelsen af formodningen var beviset fra Tait ( eng. William W. Tait ; født i 1929) for fjernelse af sektioner i andenordens logik i 1966 [2] . I 1967 blev resultatet generaliseret i Takahashi [3] og Prawitz ( svenske Dag Prawitz ; født 1936), således blev hypotesen fuldstændig bekræftet.
Senere blev fjerneligheden af sektioner opdaget for bredere klasser af kalksten, især Dragalin etablerede fjernelse af sektioner for en række ikke-klassiske logikker af højere orden, og Girard ( fr. Jean-Yves Girard ) - for systemet F .