Reverse mathematics studies which natural subsystems of second order arithmetic are equivalent to key theorems of ordinary or non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of various weak foundations for mathematics (finitistic reductionism, predicativism, predicative reductionism) in a formally precise manner.
Recursion theorist Richard Shore has proposed an alternative framework in which to conduct reverse mathematics, called computational reverse mathematics. Instead of provable equivalence over the weak base theory RCA0, the equivalence relation used in computational reverse mathematics is model-theoretic: two statements are computably equivalent iff they have the same Turing ideals (omega-models closed under Turing reducibility and recursive joins).
Despite some attractive features, computational reverse mathematics is inappropriate for foundational analysis, since the computable entailment relation it employs is Pi^1_1-complete. By internalising the proof of this theorem within the weak base theory RCA0 we can see that the existence of the truth set for computable entailment is equivalent to Pi^1_1 comprehension: a strong system which outstrips the resources which proof-theoretically weaker foundational programmes can draw upon.
Dr Walter Dean
Department of Philosophy
University of Warwick