Elementary function arithmetic: Difference between revisions

Revision as of 16:58, 20 October 2010

Revision as of 17:02, 20 October 2010

Line 1:

In [[proof theory]], a branch of [[mathematical logic]], [[Harvey Friedman]]'s''elementary function arithymetic'''grand conjectureor '''EFA''' impliesis thatthe manyweak mathematicalfragment theoremsof [[Peano Arithmetic]] with the usual elementary properties of 0,&nbsp;1,&nbsp;+,&nbsp;&times;,&nbsp;''x''<sup>''y'', together with the suchscheme asof [[Fermat's lastmathematical theoreminduction|induction]], canfor be provedformulas inwith very weakbounded systemsquantifiers.

==Friedman's grand conjecture==

[[Harvey Friedman]]'s '''grand conjecture''' implies that many mathematical theorems, such as [[Fermat's last theorem]], can be proved in very weak systems.

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;''x''&times;,&nbsp;exp, together with the scheme of [[mathematical induction|induction]] for all formulas in the language all of whose quantifiers are bounded."

==References==