Congettura di Takeuti

In logica matematica, la congettura di Takeuti è una congettura introdotta dal matematico giapponese Gaisi Takeuti. Essa afferma che ogni formalizzazione della logica di secondo ordine nel calcolo dei sequenti gode dell'eliminazione del taglio. Un'estensione naturale di tale congettura richiede che l'eliminazione del taglio valga per ogni formalizzazione nel calcolo dei sequenti di ogni logica di ordine finito.

Per la logica di secondo ordine, la congettura fu dimostrata da Tait nel 1966, sulla base di precedenti lavori di Schütte. La versione generalizzata fu dimostrata indipendentemente da Prawitz nel 1968, e da Takahashi nel 1967. Tutte e tre le dimostrazioni sfruttano tecniche semantiche. Una dimostrazione sintattica fu invece offerta da Jean-Yves Girard, nel cui sistema F la congettura risulta essere un corollario del teorema di normalizzazione forte.

La congettura di Takeuti è equivalente alla consistenza dell'aritmetica di secondo ordine, nonché alla normalizzazione forte del sistema F.

Bibliografia

• Dag Prawitz, 1968. Hauptsatz for higher order logic. J. Symb. Log., 33:452–457, 1968.
• William W. Tait, 1966. A nonconstructive proof of Gentzen's Hauptsatz for second order predicate logic. In Bulletin of the American Mathematical Society, 72:980–983.
• Gaisi Takeuti, 1953. On a generalized logic calculus. In Japanese Journal of Mathematics, 23:39–96. An errata to this article was published in the same journal, 24:149–156, 1954.
• Moto-o Takahashi, 1967. A proof of cut-elimination in simple type theory. In Japanese Mathematical Society, 10:44–45.