Elementary function arithmetic: Difference between revisions

Revision as of 01:11, 25 October 2010

Revision as of 02:50, 8 November 2010

Line 32:

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]] {{harv|Simpson|2009}}.

Elementary recursive arithmetic (ERA) is a subsystem of [[primitive recursive arithmetic]] in which recursion is restricted to [[ELEMENTARY#Definition|bounded sums and products]]. This also has the same Π{{su|p=0|b=2}} sentences as EFA, in the sense that whenever EFA proves ∀x∃y P(x,y), with P quantifier-free, ERA proves the open formula P(x,T(x)), with T a term definable in ERA.

== See also ==