Samiksha Jaiswal (Editor)

Takeuti's conjecture

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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 of arithmetic; 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.

    References

    Takeuti's conjecture Wikipedia
    (Text) CC BY-SA