Elementary Function Arithmetic (EFA)

Origin. The theory IΔ₀+exp emerged from the study of weak fragments in the Paris–Wilkie school of the 1970s and 1980s. It acquired its programmatic importance from Harvey Friedman's grand conjecture (FOM posting, 1999): every theorem published in the Annals of Mathematics whose statement involves only finitary objects can be proved in EFA. Avigad's "Number theory and elementary arithmetic" (2003) is the standard case for the conjecture's plausibility.

Models. Arithmetic in which exponentiation is total and nothing above it is. Induction is available only for bounded formulas, so the theory cannot prove the totality of the iterated exponential 2^2^⋰ — yet it proves essentially everything a number theorist writes down. That gap between what EFA cannot prove and what nobody needs proved is the conjecture's content, and it makes EFA the candidate for "what ordinary finitary mathematics actually uses".

Formalism.

Language: 0, 1, +, ×, exp (or 2ˣ), <

Axioms:

• The quantifier-free (open) axioms for 0, 1, +, ×, <
• Exponentiation: x⁰ = 1, x^(y+1) = xʸ · x
• Δ₀-induction (bounded induction): φ(0) ∧ ∀x(φ(x) → φ(x+1)) → ∀x φ(x), for each φ all of whose quantifiers are bounded (∀x ≤ t, ∃x ≤ t), possibly with free variables.

Equivalently: EFA = IΔ₀ + exp. The exponential axiom is not derivable from IΔ₀ — IΔ₀ ⊬ ∀x∀y ∃z (z = xʸ) — so it is a genuine addition and the theory it produces is genuinely stronger.

Proof-theoretic ordinal: ω³.

Position in the hierarchy: Q < IΔ₀ < EFA = IΔ₀+exp < PRA < IΣ₁ < ⋯ < PA EFA is strictly below PRA: PRA proves the totality of every primitive recursive function, EFA only of the elementary (Kalmár) ones.

Provably total functions: exactly the Kalmár elementary functions — those built from 0, S, +, ∸, ×, bounded sums and products, and composition; equivalently, computable in time bounded by a fixed tower 2^2^⋰^n.

Elementary recursive arithmetic (ERA): the quantifier-free counterpart, related to EFA as PRA is to IΣ₁ — ERA and EFA prove the same Π⁰₂ sentences, and whenever EFA ⊢ ∀x∃y P(x,y) with P quantifier-free, ERA proves P(x, T(x)) for an ERA-definable term T.

Second-order forms: RCA₀ and WKL₀, used in reverse mathematics as bases below RCA₀.

Friedman's grand conjecture: implies Fermat's Last Theorem is provable in EFA. Known natural statements not provable in EFA: consistency statements (Con(EFA) itself, by Gödel II), the Szemerédi regularity lemma, the graph minor theorem. The conjecture is open and its interest is that natural counterexamples are hard to find, not that none exist.

Symbols.

Metatheory. EFA is the natural base for arithmetized metamathematics: it proves the Gödel incompleteness theorems, the cut-elimination theorem for predicate logic, and enough of the theory of syntax to formalize everything the incompleteness argument requires, while remaining far below PA. Its ordinal ω³ compares to PRA's ω^ω and PA's ε₀, and the whole distance from EFA to PA is invisible to ordinary number theory if Friedman is right. Con(EFA) is unprovable in EFA and provable in PRA; the totality of the iterated exponential is unprovable in EFA and provable in PRA, and these are the two standard witnesses to the gap. The theory is finitely axiomatizable — unlike PA and PRA — which matters for the interpretability arguments it is used in.

Applies to. Reverse mathematics below RCA₀, via RCA₀ and WKL₀. Formalized metamathematics, where EFA is the standard base theory for consistency and incompleteness statements. Bounded arithmetic and proof complexity, as the theory just above IΔ₀. Feasible analysis. The question of how much strength ordinary number theory consumes — the entire point of Friedman's conjecture.

Limitations. Cannot prove the totality of superexponentiation, so any argument that iterates exponentiation unboundedly is out of reach — this excludes proofs by cut-elimination on their own formalization, and excludes the standard proofs of several Ramsey-theoretic statements. The grand conjecture is a conjecture; the known counterexamples (regularity lemma, graph minor theorem) show the boundary is real, and there is no argument that natural mathematics stays inside it — only the observation that it usually does. Bounded induction makes formalization awkward: statements must be arranged so their quantifiers stay bounded, and that is a nontrivial rewriting cost.

© 2026 Lingenic LLC