Elementary function arithmetic: Difference between revisions

Revision as of 15:52, 13 May 2018

Revision as of 12:36, 8 December 2018

Line 24:

: "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, 1, +, ×, 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]], and Tarjan's algorithm for the [[disjoint-set data structure]].

==Related systems==