Revision as of 13:24, 22 October 2010 edit R.e.b. (talk \| contribs) Extended confirmed users, Pending changes reviewers 42,907 edits →Friedman's grand conjecture: define ← Previous edit		Revision as of 13:29, 22 October 2010 edit undo R.e.b. (talk \| contribs) Extended confirmed users, Pending changes reviewers 42,907 edits m →Definition: fmt Next edit →
Line 7: ==Definition== EFA is a 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''<sup>''y''</sup>, ~~and often has~~ a binary relation symbol < (~~which~~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)&and;... in the usual way. Line 15 ⟶ 18: The axioms for exponentiation: ''x''<sup>0</sup> = 1, ''x''<sup>''y''+1</sup> = ''x''<sup>''y''</sup>×''x''. *Induction for formulas all of whose quantifiers are bounded (but which may contain free variables). ==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 such as EFA.

Elementary function arithmetic: Difference between revisions