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: 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.
This mathematical logic-related article is a stub.
You can help Wikipedia by expanding it.This logic-related article is a stub.