Takeuti's conjecture explained
In mathematics, Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination (Takeuti 1953). It was settled positively:
- By Tait, using a semantic technique for proving cut-elimination, based on work by Schütte (Tait 1966);
- Independently by Prawitz (Prawitz 1968) and Takahashi (Takahashi 1967) by a similar technique (Takahashi 1967) - although Prawitz's and Takahashi's proofs are not limited to second-order logic, but concern higher-order logics in general;
- It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F.
Takeuti's conjecture is equivalent to the 1-consistency of second-order arithmetic in the sense that each of the statements can be derived from each other in the weak system PRA. It is also equivalent to the strong normalization of the Girard/Reynold's System F.
See also
References
- 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.
