# [FOM] Two questions about proof theoretic reductions

Aatu Koskensilta aatu.koskensilta at xortec.fi
Fri May 7 13:24:29 EDT 2004

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