Elementary function arithmetic: Difference between revisions

Revision as of 20:27, 22 August 2023

Revision as of 20:31, 22 August 2023

Line 10:

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

*two constants 0, 1,

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

*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).

'''Bounded quantifiers''' are those of the form {{<math|∀>\forall(x < y)}}</math> and {{<math|∃>\exists(x < y)}}</math> which are abbreviations for {{<math|∀>\forall x (x < y) → ...}}\rightarrow\ldots</math> and {{<math|∃x>\exists x(x < y)∧...}}\land\ldots</math> in the usual way.

The axioms of EFA are

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

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

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