Elementary Function Arithmetic

In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Friedman's Research on the Foundations of Mathematics'' (1985), Studies in Logic and the Foundations of Mathematics vol. 117. is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ''x''^''y'', together with induction for formulas with bounded quantifiers.

EFA is a very weak logical system, whose proof theoretic ordinal is ω³, 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 ''x''^''y'',
*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 and which are abbreviations for and in the usual way.

The axioms of EFA are
*The axioms of Robinson arithmetic for 0, 1, +, ×, <
*The axioms for exponentiation: ''x''⁰ = 1, ''x''^''y''+1 = ''x''^''y'' × ''x''.
*Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).

Friedman's grand conjecture

Harvey Friedman's grand conjecture implies that many mathematical theorems, such as Fermat's Last Theorem