Elementary function arithmetic: Difference between revisions

Revision as of 16:37, 24 April 2018

Revision as of 15:52, 13 May 2018

Line 1:

{{No footnotes|date=November 2017}}

In [[proof theory]], a branch of [[mathematical logic]], '''elementary function arithmetic''', also called '''EFA''', '''elementary arithmetic''' and '''exponential function arithmetic''', is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ''x''^''y'', together with [[mathematical induction|induction]] for formulas with [[bounded quantifiersquantifier]]s.

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 [[Peano axioms|first-order arithmetic]].