Content deleted Content added
ref |
→Friedman's grand conjecture: define |
||
Line 5:
There are weak fragments of second-order arithmetic called RCA{{su|p=*|b=0}} and WKL{{su|p=*|b=0}} that have the same consistency strength as EFA and are conservative over it for Π{{su|p=0|b=2}} sentences, which are sometimes studied in [[reverse mathematics]] {{harvtxt|Simpson|2009}}.
==Definition==
EFA is a a system in first order logic (with equality). Its language contains constants 0, 1, binary operations +, ×, exp, with exp(''x'',''y'') usually written as ''x''<sup>''y''</sup>, and often has a relation symbol < (which is not really necessary as it can be written in terms of the other operations, 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, +, ×, <
*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.
| |||