Elementary function arithmetic: Difference between revisions

Revision as of 04:58, 1 January 2013

Revision as of 00:48, 7 June 2013

Line 1:

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 and was developed by [[Harvey Friedman|Harvey Friedman]].

In [[proof theory]], a branch of [[mathematical logic]], '''elementary function arithmetic''' or '''exponential function arithmetic (EFA)''' is the system of arithmetic with the usual elementary properties of 0, 1, +, ×, ''x''^''y'', together with [[mathematical induction|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==