Content deleted Content added
m →Definition: fmt |
related systems |
||
Line 2:
EFA is a very weak logical system, whose [[proof theoretic ordinal]] is ω<sup>3</sup>, but still seems able to prove much of ordinary mathematics that can be stated in the language of first-order arithmetic.
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==
Line 27 ⟶ 25:
While it is easy to construct artificial arithmetical statements that are try but not provable in EFA, 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 [[Szemeredi's lemma]] and the [[graph minor theorem]], and Tarjan's algorithm for the [[disjoint-set data structure]].
==Related systems==
One can omit the binary function symbol exp from the language, by taking Robinson arithmetic together with induction for all formulas with bounded quantifiers and an axiom stating roughly that exponentiation is a function defined everywhere. This is similar to EFA and has the same proof theoretic strength, but is more cumbersome to work with.
▲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]] {{
== See also ==
| |||