Elementary function arithmetic

<p>In <a href="http://en.wikipedia.org/wiki/Proof_theory" title="Proof theory">proof theory</a>, a branch of <a href="http://en.wikipedia.org/wiki/Mathematical_logic" title="Mathematical logic">mathematical logic</a>, <b>elementary function arithmetic</b> or <b>exponential function arithmetic</b> (<b>EFA</b>) is the system of arithmetic with the usual elementary properties of 0,&nbsp;1,&nbsp;+,&nbsp;×,&nbsp;<i>x</i>^<i>y</i>, together with <a href="http://en.wikipedia.org/wiki/Mathematical_induction" title="Mathematical induction">induction</a> for formulas with bounded quantifiers.

EFA is a very weak logical system, whose <a href="http://en.wikipedia.org/wiki/Proof_theoretic_ordinal" title="Proof theoretic ordinal" class="mw-redirect">proof theoretic ordinal</a> is ω³, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.

&nbsp;</p>

<h2>Definition</h2>

<p>EFA is a system in first order logic (with equality). Its language contains:</p>

<ul>

<li>two constants 0, 1,</li>

<li>three binary operations +, ×, exp, with exp(<i>x</i>,<i>y</i>) usually written as <i>x</i>^<i>y</i>,</li>

<li>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).</li>

</ul>

<p>Bounded quantifiers are those of the form ∀(x<y) and ∃ (x<y) which are abbreviations for ∀ x (x<y)→,,, and ∃x (x<y)∧... in the usual way.

The axioms of EFA are</p>

<ul>

<li>The axioms of <a href="http://en.wikipedia.org/wiki/Robinson_arithmetic" title="Robinson arithmetic">Robinson arithmetic</a> for 0, 1, +, ×, <</li>

<li>The axioms for exponentiation: <i>x</i>⁰ = 1, <i>x</i>^<i>y</i>+1 = <i>x</i>^<i>y</i>×<i>x</i>.</li>

<li>Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).</li>

</ul>

<p>&nbsp;</p>