Show description

E. requires at most some instances of induction and collection beyond Proof: E. 2. M. BEESON 46 Remark: In case T is a non-extensional theory, we can allow an arbitrary formula in place of a definable set in the rule of local continuity, local uniform continuity, and continuous choice. We now shall obtain some consistency results complementing these results on derived rules. These results concern the principles corresponding to the derived rules we have already studied; their statements are obtained from the rules in the obvious way, namely: if a rule says, from A infer B, then the corresponding principle 1 s A + B.

YEa)}; that is, This can be formed using separation and abstrac- {€a' : p((-(B(y) & yea)}. 4. @/l-(xaa -+ 3n,mEw(x=). The last two conjuncts can be verified simi- To check A -separation, we have to prove that pl(-B(y) is a A formula if is; this is a simple induction on the complexity of 8. rhe definition of x' just given also determines the term t' corresponding to the It has to be checked that x' as term t associated with this separation axiom. just defined is a good set. Generally if x' is defined as {: p//-C) then x' is good, since if q 2 and p is in x', then q also forces C, so is in x', by definition of x i ;but cq,y'/q> is exactly what we , which is must prove is in x' in order to show x' is good.

A s r e g a r d s power s e t : when c o n s i d e r i n g t h e o r i e s with power s e t , t h e r e is no need t o use t h e complicated f o r c i n g i n t e r p r e t a t i o n given h e r e ; i n s t e a d , one should r e t u r n t o t h e simpler d e f i n i t i o n f i r s t given. With t h a t d e f i n i t i o n , t h e v e r i f i c a t i o n of power set i s a l s o completely s t r a i g h t f o r w a r d . 1. Lemma 6 . 6 L e t A be a r i t h m e t i c i n 5, b u t n o t c o n t a i n i n g formula of second o r d e r a r i t h m e t i c ) .