Elementary function arithmetic: Difference between revisions

Revision as of 16:53, 18 April 2021

Revision as of 20:18, 18 April 2021

Line 1:

{{No footnotes|date=November 2017}}

{{redirect|Elementary recursive arithmetic|the computational complexity class|ELEMENTARY}}

In [[proof theory]], a branch of [[mathematical logic]], '''elementary function arithmetic''' ('''EFA'''), also called '''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 quantifier]]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]].

Line 8:

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

*two constants 0, 1,

*three binary operations +, ××, exp, with exp(''x'',''y'') usually written as ''x''^''y'',

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

'''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

*The axioms of [[Robinson arithmetic]] for 0, 1, +, &times;×, <

*The axioms for exponentiation: ''x''⁰ = 1, ''x''^''y''+1 = ''x''^''y'' &times;× ''x''.

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

Line 23:

The original statement of the conjecture from {{harvtxt|Friedman|1999}} is:

: "Every theorem published in the ''[[Annals of Mathematics]]'' whose statement involves only finitary mathematical objects (i.e., what logicians call an arithmetical statement) can be proved in EFA. EFA is the weak fragment of [[Peano Arithmetic]] based on the usual quantifier-free axioms for 0,&nbsp;1,&nbsp;+,&nbsp;&times;×,&nbsp;exp, together with the scheme of [[mathematical induction|induction]] for all formulas in the language all of whose quantifiers are bounded."

While it is easy to construct artificial arithmetical statements that are true but not provable in EFA{{example needed|date=December 2018}}, the point of Friedman's conjecture is that natural examples of such statements in mathematics seem to be rare. Some natural examples include consistency statements from logic, several statements related to [[Ramsey theory]] such as the [[Szemerédi regularity lemma]] and the [[graph minor theorem]].