Conservation Results

In this section we generalize the construction of §1 to a wider setting. We then use this idea to obtain some conservation results involving the scheme (*) of Theorem 1.3.

Two important subsystems of second order arithmetic are (arithmetical transfinite recursion with restricted induction) and - (the transfinite induction scheme). For general background, see Simpson [5]. It is known [5, § VII.2] that - , and that every -model is a model of - .

Let
be a countable model of
,
where
.
Define
is a finite
subset of
and there exists
meeting .
The notion of
being *generic over*
is
defined in the obvious way. As in §1, the basic forcing
lemmas can be proved. Let
be generic
over
.
Put
.

*Proof.*The proof is a straightforward generalization of the arguments of
§1.

*Proof.*Write
as
for some fixed .
If
,
then for each
we have
that
is
dense in
,
hence
.
Thus
,
i.e.,
,
so
.

We now have:

*Proof.*Let
be a
sentence. Suppose
.
Let
be a countable
model of
.
Let
as above. Since
is a
sentence, we have
by Lemmas 2.1 and 2.2 that
.
Thus
.

In order to obtain a similar result for - , we first prove:

*Proof.*Recall from [5, §§VIII.3 and VIII.6] that all of the
basic results of hyperarithmetical theory are provable in
.
In particular, by [5, Theorem VIII.6.7], the
Gandy/Kreisel/Tait Theorem holds in
.
Thus for all
we have

there exists
meeting *p* such that
.

Now, it is provable in
that the predicate
is
.
Thus we have
,
i.e.,
``all ordinals are recursive''. This
proves our lemma.

*Proof.*By Lemma 2.5 it suffices to prove: if
transfinite induction for recursive well
orderings, then
transfinite induction for
recursive well orderings. Let
be such that
``<_{e} is a recursive well ordering''.
Suppose
and
.
Put
.
Clearly
.
By definability of forcing, *A* is
definable over
.
Hence there exists
such
that
``*a* is the <_{e}-least element of
*A*''. For each *n*<_{e}*a* we have
,
but
,
so let
be such that
.
Then
``*a* is the <_{e}-least
*n* such that
''. Thus
transfinite induction for recursive well orderings.