The general enterprise of calibrating the strength of classical mathematical theorems in terms of the axioms, typically of set existence, needed to prove them; originated in its modern form in the 1970s by H. Friedman and S. G. Simpson (see R.A. Shore, "Reverse Mathematics: The Playground of Logic", ...
Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include Subsystems of Second Order Arithmetic ...
According to the Wikipedia ACA0 is a conservative extension of First Order logic + PA. http://en.wikipedia.org/wiki/Reverse_Mathematics First of all I have a few questions about the proof: a - What ...
A definition is called impredicative if it involves quantification over a domain that contains the thing being defined. For instance, if you define hereditary property to be a property which applies ...
In the 1960's, Feferman and Schutte did groundbreaking proof-theoretic work to find out the strength of predicative systems of second-order arithmetic. They used the ramified theory of types, a ...
In their article "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" (American Mathematical Monthly, April 2013), Nyman and Su write "[W]e are unaware of a direct proof that Tucker's ...
(Base theory $RCA_0$)The principle says there exists a function g such that g dominates any X-recursive function for any X in the model. i.e. For any $f\le_T X$, $\exists b\in M$ such that ...
Second-Order Arithmetic is considered impredicative, because the comprehension scheme allows formulas with bound second-order variables that range over all sets of natural numbers, including the set ...