In
mathematics
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
, 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 on ...
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 part I of his landmark 1935 paper "Investigations in Logical De ...
(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 logic
In mathematics and logic, a higher-order logic (abbreviated HOL) is a form of logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are m ...
s 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 a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the Éc ...
'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 polymorph ...
.
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 of mathematics, foundation for much, but not all, ...
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
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 polymorph ...
.
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 arithmetic is consistent – free of any internal contradictions. Hilbert stated that the axioms he considered fo ...
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, and for his contributions to proof-theoretic semantics.
Prawitz is a member of the ...
, 1968. Hauptsatz for higher order logic. ''
Journal of Symbolic Logic
The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by '' Mathematical Reviews'', Zent ...
'', 33:452–457, 1968.
*
William W. Tait
William Walker Tait (January 22, 1929 – March 15, 2024) was an American philosopher. He was 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 ...
, 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 o ...
'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