In proof theory, a branch of mathematical logic, elementary function arithmetic or EFA is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, xy, together with induction for formulas with bounded quantifiers.
Friedman's grand conjecture
Harvey Friedman's grand conjecture implies that many mathematical theorems, such as Fermat's last theorem, can be proved in very weak systems.
The original statement of the conjecture from Friedman (1999) is:
- "Every theorem published in the Annals of Mathematics 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 induction for all formulas in the language all of whose quantifiers are bounded."
References
- Avigad, Jeremy (2003), "Number theory and elementary arithmetic", Philosophia Mathematica. Philosophy of Mathematics, its Learning, and its Application. Series III, 11 (3): 257–284, doi:10.1093/philmat/11.3.257, ISSN 0031-8019, MR 2006194
- Friedman, Harvey (1999), grand conjectures