Takeuti's conjecture

EN Texto em inglês Ainda não há artigo no seu idioma: trecho em inglês.

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). It is also equivalent to the strong normalization of the Girard/Reynold's System F.