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 . 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
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<ea we have , but , so let be such that . Then ``a is the <e-least n such that ''. Thus transfinite induction for recursive well orderings.