Takeuti conjecture
Encyclopedia
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 consistency of second-order arithmetic
and to the strong normalization of the Girard/Reynold's System F
.
Gaisi Takeuti
is a Japanese mathematician, known for his work in proof theory.After graduating from Tokyo University, he went to Princeton to study under Kurt Gödel.He later became a professor at the University of Illinois at Urbana-Champaign...
that a sequent formalisation of second-order logic
Second-order logic
In logic and mathematics second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory....
has cut-elimination
Cut-elimination theorem
The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively...
(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 Takahashi by a similar technique (Takahashi 1967);
- It is a corollary of Jean-Yves GirardJean-Yves GirardJean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
's syntactic proof of strong normalization for System FSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
.
Takeuti's conjecture is equivalent to the consistency of second-order arithmetic
Second-order arithmetic
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
and to the strong normalization of the Girard/Reynold's System F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
.