Content deleted Content added
No edit summary |
Citing statement that names denote the same theory |
||
Line 2:
{{No footnotes|date=November 2017}}
{{redirect|Elementary recursive arithmetic|the computational complexity class|ELEMENTARY}}
In [[proof theory]], a branch of [[mathematical logic]], '''elementary function arithmetic''' ('''EFA'''), also called '''elementary arithmetic''' and '''exponential function arithmetic'''<ref>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.</ref>, is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ''x''<sup>''y''</sup>, together with [[mathematical induction|induction]] for formulas with [[bounded quantifier]]s.
EFA is a very weak logical system, whose [[proof theoretic ordinal]] is ω<sup>3</sup>, but still seems able to prove much of ordinary mathematics that can be stated in the language of [[Peano axioms|first-order arithmetic]].
| |||