Elementary function arithmetic: Difference between revisions

Revision as of 20:31, 22 August 2023

Revision as of 20:32, 22 August 2023

Line 9:

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

*two constants <math>0</math>, <math>1</math>,

*three binary operations <math>+</math>, ×<math>\times</math>, <math>\textrm{exp}</math>, with <math>\textrm{exp}(x,y)</math> usually written as <math>x^y</math>,

*a binary relation symbol <math>< </math> (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).

Line 16:

The axioms of EFA are

*The axioms of [[Robinson arithmetic]] for <math>0</math>, <math>1</math>, <math>+</math>, <math>×\times</math>, <math>< </math>

*The axioms for exponentiation: <math>x^0=1</math>, <math>x^{y+1}=x^y\times x</math>.

*Induction for formulas all of whose quantifiers are bounded (but which may contain free variables).