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 (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 Prawitz (Prawitz 1968) and Takahashi by a similar technique (Takahashi 1967), 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).