Grand conjecture
Encyclopedia
In proof theory
, a branch of mathematical logic
, elementary function arithmetic or exponential function arithmetic (EFA) is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, xy, together with induction
for formulas with bounded quantifiers.
EFA is a very weak logical system, whose proof theoretic ordinal is ω3, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.
Bounded quantifiers are those of the form ∀(x
The axioms of EFA are
's grand conjecture implies that many mathematical theorems, such as Fermat's last theorem
, can be proved in very weak systems such as EFA.
The original statement of the conjecture from is:
While it is easy to construct artificial arithmetical statements that are true but not provable in EFA, the point of Friedman's conjecture is that natural examples of such statements in mathematics seem to be rare. Some natural examples include consistency statements from logic, several statements related to Ramsey theory
such as Szemeredi's lemma and the graph minor theorem, and Tarjan's algorithm for the disjoint-set data structure
.
There are weak fragments of second-order arithmetic called RCA and WKL that have the same consistency strength as EFA and are conservative over it for Π sentences, which are sometimes studied in reverse mathematics
.
Elementary recursive arithmetic (ERA) is a subsystem of primitive recursive arithmetic
in which recursion is restricted to bounded sums and products. This also has the same Π sentences as EFA, in the sense that whenever EFA proves ∀x∃y P(x,y), with P quantifier-free, ERA proves the open formula P(x,T(x)), with T a term definable in ERA.
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, a branch of mathematical logic
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, elementary function arithmetic or exponential function arithmetic (EFA) is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, xy, together with induction
Mathematical induction
Mathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
for formulas with bounded quantifiers.
EFA is a very weak logical system, whose proof theoretic ordinal is ω3, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.
Definition
EFA is a system in first order logic (with equality). Its language contains:- two constants 0, 1,
- three binary operations +, ×, exp, with exp(x,y) usually written as xy,
- a binary relation symbol < (This is not really necessary as it can be written in terms of the other operations and is sometimes omitted, but is convenient for defining bounded quantifiers).
Bounded quantifiers are those of the form ∀(x
The axioms of EFA are
- The axioms of Robinson arithmeticRobinson arithmeticIn mathematics, Robinson arithmetic, or Q, is a finitely axiomatized fragment of Peano arithmetic , first set out in R. M. Robinson . Q is essentially PA without the axiom schema of induction. Since Q is weaker than PA, it is incomplete...
for 0, 1, +, ×, < - The axioms for exponentiation: x0 = 1, xy+1 = xy×x.
- Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).
Friedman's grand conjecture
Harvey FriedmanHarvey Friedman
Harvey Friedman is a mathematical logician at Ohio State University in Columbus, Ohio. He is noted especially for his work on reverse mathematics, a project intended to derive the axioms of mathematics from the theorems considered to be necessary...
's grand conjecture implies that many mathematical theorems, such as Fermat's last theorem
Fermat's Last Theorem
In number theory, Fermat's Last Theorem states that no three positive integers a, b, and c can satisfy the equation an + bn = cn for any integer value of n greater than two....
, can be proved in very weak systems such as EFA.
The original statement of the conjecture from is:
- "Every theorem published in the Annals of MathematicsAnnals of MathematicsThe Annals of Mathematics is a bimonthly mathematical journal published by Princeton University and the Institute for Advanced Study. It ranks amongst the most prestigious mathematics journals in the world by criteria such as impact factor.-History:The journal began as The Analyst in 1874 and was...
whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of Peano Arithmetic based on the usual quantifier-free axioms for 0, 1, +, ×, exp, together with the scheme of inductionMathematical inductionMathematical induction is a method of mathematical proof typically used to establish that a given statement is true of all natural numbers...
for all formulas in the language all of whose quantifiers are bounded."
While it is easy to construct artificial arithmetical statements that are true but not provable in EFA, the point of Friedman's conjecture is that natural examples of such statements in mathematics seem to be rare. Some natural examples include consistency statements from logic, several statements related to Ramsey theory
Ramsey theory
Ramsey theory, named after the British mathematician and philosopher Frank P. Ramsey, is a branch of mathematics that studies the conditions under which order must appear...
such as Szemeredi's lemma and the graph minor theorem, and Tarjan's algorithm for the disjoint-set data structure
Disjoint-set data structure
In computing, a disjoint-set data structure is a data structure that keeps track of a set of elements partitioned into a number of disjoint subsets. A union-find algorithm is an algorithm that performs two useful operations on such a data structure:* Find: Determine which set a particular element...
.
Related systems
One can omit the binary function symbol exp from the language, by taking Robinson arithmetic together with induction for all formulas with bounded quantifiers and an axiom stating roughly that exponentiation is a function defined everywhere. This is similar to EFA and has the same proof theoretic strength, but is more cumbersome to work with.There are weak fragments of second-order arithmetic called RCA and WKL that have the same consistency strength as EFA and are conservative over it for Π sentences, which are sometimes studied in reverse mathematics
Reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of...
.
Elementary recursive arithmetic (ERA) is a subsystem of primitive recursive arithmetic
Primitive recursive arithmetic
Primitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist...
in which recursion is restricted to bounded sums and products. This also has the same Π sentences as EFA, in the sense that whenever EFA proves ∀x∃y P(x,y), with P quantifier-free, ERA proves the open formula P(x,T(x)), with T a term definable in ERA.
See also
- ELEMENTARY, a related computational complexity class
- Grzegorczyk hierarchyGrzegorczyk hierarchyThe Grzegorczyk hierarchy , named after the Polish logician Andrzej Grzegorczyk, is a hierarchy of functions used in computability theory . Every function in the Grzegorczyk hierarchy is a primitive recursive function, and every primitive recursive function appears in the hierarchy at some level...
- Reverse mathematicsReverse mathematicsReverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in contrast to the ordinary mathematical practice of...
- Tarski's high school algebra problemTarski's high school algebra problemIn mathematical logic, Tarski's high school algebra problem was a question posed by Alfred Tarski. It asks whether there are identities involving addition, multiplication, and exponentiation over the positive integers that cannot be proved using eleven axioms about these operations that are taught...