In
mathematics, Takeuti's conjecture is the conjecture of
Gaisi Takeuti
was 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. Take ...
that a sequent formalisation of
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.
First-order logic quantifies ...
has
cut-elimination
The cut-elimination theorem (or Gentzen's ''Hauptsatz'') is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark 1934 paper "Investigations in Logical Deduction" for ...
(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 (Takahashi 1967) 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
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of th ...
's syntactic proof of strong normalization for
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
.
Takeuti's conjecture is equivalent to the 1-consistency of
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.
A precu ...
in the sense that each of the statements can be derived from each other in the weak system
PRA. It is also equivalent to the
strong normalization
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
of the Girard/Reynold's
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
.
See also
*
Hilbert's second problem
In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that the arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he conside ...
References
*
Dag Prawitz
Dag Prawitz (born 1936, Stockholm) is a Swedish philosopher and logician. He is best known for his work on proof theory and the foundations of natural deduction.
Prawitz is a member of the Norwegian Academy of Science and Letters, of the Roya ...
, 1968. Hauptsatz for higher order logic. J. Symb. Log., 33:452–457, 1968.
*
William W. Tait
William Walker Tait (born 1929) is an emeritus professor of philosophy at the University of Chicago, where he served as a faculty member from 1972 to 1996, and as department chair from 1981 to 1987.
Education and career
Tait received his B.A. f ...
, 1966. A nonconstructive proof of
Gentzen
Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
's Hauptsatz for second order predicate logic. In ''
Bulletin of the American Mathematical Society
The ''Bulletin of the American Mathematical Society'' is a quarterly mathematical journal published by the American Mathematical Society.
Scope
It publishes surveys on contemporary research topics, written at a level accessible to non-experts. ...
'', 72:980–983.
*
Gaisi Takeuti
was 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. Take ...
, 1953. On a generalized logic calculus. In ''Japanese Journal of Mathematics'', 23:39–96. An errata to this article was published in the same journal, 24:149–156, 1954.
* Moto-o Takahashi, 1967. A proof of cut-elimination in simple type theory. In ''Japanese Mathematical Society'', 10:44–45.
Proof theory
Conjectures that have been proved
{{logic-stub