[FOM] Two questions about proof theoretic reductions

[Aatu Koskensilta]

A theory T_1 can be conservative over some theory T_2 with  respect to 
some class of formulas F, meaning that if T_1 |- f and f \in F, then T_2 
|- f.

If this is to be epistemologically interesting, a stronger condition is 
needed, namely that of proof theoretic reducibility. The basic idea is 
that if we are to be entitled (based on principles formalised in T_2) to 
use T_1 when deriving F-theorems, the conservativity should be provable 
in T_2. Feferman gives the following definition:

 T_1 is proof theoretically reducible to T_2 for a class of formulas F,
 T_1 < T_2 [F], if there is a recursive function f, s.t.

  1) if p is a proof of f \in F in T_1, then f(p) is a proof of f in T_2
  2) the above is provable in T_2

We know that for example WKL_0 < PRA [Pi_2] (if I recall correctly) and 
that ATR_0 < IR [Pi1_1] (ATR_0 is a subsystem of second order arithmetic 
embodying definition by arithmetic transfinite recursion and IR is 
Feferman's system of predicative analysis).

First question
-----------------
My first question is whether there are any interesting and natural 
theories T_1 and T_2, such that T_1 is conservative over T_2 for some 
class of formulas F, but T_1 < T_2 [F] does not hold.

It's not difficult to come up with a contrived example. For example, let 
H(x) = a formula defining the epsilon-zeroth function E in the 
Gregrorzyck hierarchy, and add to PA the set of sentences {Cons(PA<H(n)) 
| n \in N }, i.e. for every n the assertion that axioms of PA of 
complexity less than E(n) form a consistent theory. PA proves all of 
these sentences, so the resulting theory T is obviously conservative 
over PA. It can't be proof theoretically reducible to PA, however, 
because proof of Cons(PA<E(n)) has (n + some constant) symbols in T, but 
must have over E(n) symbols in PA. Hence the function sending proofs in 
T to proofs in PA grows faster than any function that can be proved 
total in PA. Of course, the only reason anyone would consider T is in 
context of my question, so it's not quite natural...

Second question
-------------------

Originally, it Hilbert's idea was to prove (abstract mathematics) < 
(finitistic mathematics) [Pi_1]. We now know this is impossible, but on 
the other hand we know that for some very interesting and natural 
theories T < PRA[Pi_2].
At first sight this seems to suggests that a finitist can safely use T 
to prove Pi_2 theorems. Presumably he would wish to do this because 
proofs are much shorter and more intelligible in T than in PRA. However, 
if PRA really captures
all finitisticly valid mathematical principles, it seems that the above 
result is not relevant to the finitist at all! This is because if we 
have a proof of T < PRA[Pi_1] in PRA we obviously can't prove (in PRA) 
the reflection principle
T |- \phi --> \phi. Why should the finitist then care about T, if he 
can't actually use it to shorten proofs? Am I correct in assuming that 
proof theoretic reductions T_1 < T_2[F] are (epistemologically) of 
interest only to those who do accept
F-soundness of T_2?

-- 
Aatu Koskensilta (aatu.koskensilta at xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 - Ludwig Wittgenstein, Tractatus Logico-Philosophicus