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:
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.
