Takeuti's conjecture

In mathematics, Takeuti's conjecture is the conjecture of Gaisi Takeuti that a sequent formalisation of second-order logic has cut-elimination. It was settled positively:

By Tait, using a semantic technique for proving cut-elimination, based on work by Schütte ;
Independently by Prawitz and Takahashi by a similar technique, 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 of primitive recursive arithmetic (PRA). It is also equivalent to the strong normalization of the Girard/Reynold's System F.