- Takeuti conjecture
Takeuti's conjecture is the conjecture of
Gaisi Takeuti that a sequent formalisation ofsecond-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 Takahashi by a similar technique (Takahashi 1967);
* It is a corollary ofJean-Yves Girard 's syntactic proof of strong normalization forSystem F .Takeuti's conjecture is equivalentfn|1 to the consistency of
second-order arithmetic and to thestrong normalization of the Girard/Reynold'sSystem F .Notes
fnb|1 Equivalent in the sense that each of the statements can be derived from each other in the weak system
PRA of arithmetic; consistency refers here to the truth of theGödel sentence for second-order arithmetic. Seeconsistency proof for more discussion.References
*
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.
Wikimedia Foundation. 2010.
