Takeuti conjecture
From Wikipedia, the free encyclopedia
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 (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 equivalent1 to the consistency of second-order arithmetic and to the strong normalization of the Girard/Reynold's System F.
[edit] Notes
Note 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 the Gödel sentence for second-order arithmetic. See consistency proof for more discussion.
[edit] References
- William 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.
 |
This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |
