1. See also

2. References

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 Takahashi by a similar technique (Takahashi 1967);
• It is a corollary of Jean-Yves Girard's syntactic proof of strong normalization for System F.

Takeuti's conjecture is equivalent to the consistency of second-order arithmetic in the sense that each of the statements can be derived from each other in the weak system PRA; consistency refers here to the truth of the Gödel sentence for second-order arithmetic. It is also equivalent to the strong normalization of the Girard/Reynold's System F.

See also

• Hilbert's second problem

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.

• Ales Prudnikau
• Ales Pus
• Ales Razym
• Ales Rebicek
• Alessandra Aguilar
• Alessandra ambrosia
• Alessandra Amoroso
• Alessandra Buonanno
• Alessandra Cappellotto
• Alessandra Celletti
• Alessandra Facchinetti
• Alessandra Fossati
• Alessandra Galiotto
• Alessandra Mastronardi
• Alessandra Melucco Vaccaro
• Alessandra Mignacca
• Alessandra Olivia Torresani
• Alessandra Panaro
• Alessandra Piccione
• Alessandra Scala
• Alessandra Schiavone De Rossi
• Alessandra Toreson
• Alessandra Toressani
• Alessandra Tornimparte
• Alessandria Challenger