tweaks
authorpaulson
Tue Sep 10 16:47:17 2002 +0200 (2002-09-10)
changeset 135637d6c9817c432
parent 13562 5b71e1408ac4
child 13564 1500a2e48d44
tweaks
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Reflection.thy
src/ZF/Constructible/Relative.thy
     1.1 --- a/src/ZF/Constructible/L_axioms.thy	Mon Sep 09 17:28:29 2002 +0200
     1.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Sep 10 16:47:17 2002 +0200
     1.3 @@ -20,26 +20,34 @@
     1.4  apply (blast intro: zero_in_Lset)
     1.5  done
     1.6  
     1.7 -lemma upair_ax: "upair_ax(L)"
     1.8 +theorem upair_ax: "upair_ax(L)"
     1.9  apply (simp add: upair_ax_def upair_def, clarify)
    1.10  apply (rule_tac x="{x,y}" in rexI)
    1.11  apply (simp_all add: doubleton_in_L)
    1.12  done
    1.13  
    1.14 -lemma Union_ax: "Union_ax(L)"
    1.15 +theorem Union_ax: "Union_ax(L)"
    1.16  apply (simp add: Union_ax_def big_union_def, clarify)
    1.17  apply (rule_tac x="Union(x)" in rexI)
    1.18  apply (simp_all add: Union_in_L, auto)
    1.19  apply (blast intro: transL)
    1.20  done
    1.21  
    1.22 -lemma power_ax: "power_ax(L)"
    1.23 +theorem power_ax: "power_ax(L)"
    1.24  apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify)
    1.25  apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)
    1.26  apply (simp_all add: LPow_in_L, auto)
    1.27  apply (blast intro: transL)
    1.28  done
    1.29  
    1.30 +text{*We don't actually need @{term L} to satisfy the foundation axiom.*}
    1.31 +theorem foundation_ax: "foundation_ax(L)"
    1.32 +apply (simp add: foundation_ax_def)
    1.33 +apply (rule rallI) 
    1.34 +apply (cut_tac A=x in foundation)
    1.35 +apply (blast intro: transL)
    1.36 +done
    1.37 +
    1.38  subsection{*For L to satisfy Replacement *}
    1.39  
    1.40  (*Can't move these to Formula unless the definition of univalent is moved
    1.41 @@ -65,7 +73,7 @@
    1.42  apply (blast intro: L_I Lset_in_Lset_succ)
    1.43  done
    1.44  
    1.45 -lemma replacement: "replacement(L,P)"
    1.46 +theorem replacement: "replacement(L,P)"
    1.47  apply (simp add: replacement_def, clarify)
    1.48  apply (frule LReplace_in_L, assumption+, clarify)
    1.49  apply (rule_tac x=Y in rexI)
     2.1 --- a/src/ZF/Constructible/Reflection.thy	Mon Sep 09 17:28:29 2002 +0200
     2.2 +++ b/src/ZF/Constructible/Reflection.thy	Tue Sep 10 16:47:17 2002 +0200
     2.3 @@ -37,16 +37,16 @@
     2.4        and Mset_cont    : "cont_Ord(Mset)"
     2.5        and Pair_in_Mset : "[| x \<in> Mset(a); y \<in> Mset(a); Limit(a) |] 
     2.6                            ==> <x,y> \<in> Mset(a)"
     2.7 -  defines "M(x) == \<exists>a. Ord(a) \<and> x \<in> Mset(a)"
     2.8 -      and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) \<and>
     2.9 +  defines "M(x) == \<exists>a. Ord(a) & x \<in> Mset(a)"
    2.10 +      and "Reflects(Cl,P,Q) == Closed_Unbounded(Cl) &
    2.11                                (\<forall>a. Cl(a) --> (\<forall>x\<in>Mset(a). P(x) <-> Q(a,x)))"
    2.12    fixes F0 --{*ordinal for a specific value @{term y}*}
    2.13    fixes FF --{*sup over the whole level, @{term "y\<in>Mset(a)"}*}
    2.14    fixes ClEx --{*Reflecting ordinals for the formula @{term "\<exists>z. P"}*}
    2.15 -  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) \<and> P(<y,z>)) --> 
    2.16 +  defines "F0(P,y) == \<mu>b. (\<exists>z. M(z) & P(<y,z>)) --> 
    2.17                                 (\<exists>z\<in>Mset(b). P(<y,z>))"
    2.18        and "FF(P)   == \<lambda>a. \<Union>y\<in>Mset(a). F0(P,y)"
    2.19 -      and "ClEx(P,a) == Limit(a) \<and> normalize(FF(P),a) = a"
    2.20 +      and "ClEx(P,a) == Limit(a) & normalize(FF(P),a) = a"
    2.21  
    2.22  lemma (in reflection) Mset_mono: "i\<le>j ==> Mset(i) <= Mset(j)"
    2.23  apply (insert Mset_mono_le) 
    2.24 @@ -56,7 +56,7 @@
    2.25  text{*Awkward: we need a version of @{text ClEx_def} as an equality
    2.26        at the level of classes, which do not really exist*}
    2.27  lemma (in reflection) ClEx_eq:
    2.28 -     "ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(FF(P),a) = a"
    2.29 +     "ClEx(P) == \<lambda>a. Limit(a) & normalize(FF(P),a) = a"
    2.30  by (simp add: ClEx_def [symmetric]) 
    2.31  
    2.32  
    2.33 @@ -72,26 +72,26 @@
    2.34  
    2.35  theorem (in reflection) And_reflection [intro]:
    2.36       "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    2.37 -      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<and> P'(x), 
    2.38 -                                      \<lambda>a x. Q(a,x) \<and> Q'(a,x))"
    2.39 +      ==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) & P'(x), 
    2.40 +                                      \<lambda>a x. Q(a,x) & Q'(a,x))"
    2.41  by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    2.42  
    2.43  theorem (in reflection) Or_reflection [intro]:
    2.44       "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    2.45 -      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), \<lambda>x. P(x) \<or> P'(x), 
    2.46 -                                      \<lambda>a x. Q(a,x) \<or> Q'(a,x))"
    2.47 +      ==> Reflects(\<lambda>a. Cl(a) & C'(a), \<lambda>x. P(x) | P'(x), 
    2.48 +                                      \<lambda>a x. Q(a,x) | Q'(a,x))"
    2.49  by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    2.50  
    2.51  theorem (in reflection) Imp_reflection [intro]:
    2.52       "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    2.53 -      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    2.54 +      ==> Reflects(\<lambda>a. Cl(a) & C'(a), 
    2.55                     \<lambda>x. P(x) --> P'(x), 
    2.56                     \<lambda>a x. Q(a,x) --> Q'(a,x))"
    2.57  by (simp add: Reflects_def Closed_Unbounded_Int, blast)
    2.58  
    2.59  theorem (in reflection) Iff_reflection [intro]:
    2.60       "[| Reflects(Cl,P,Q); Reflects(C',P',Q') |] 
    2.61 -      ==> Reflects(\<lambda>a. Cl(a) \<and> C'(a), 
    2.62 +      ==> Reflects(\<lambda>a. Cl(a) & C'(a), 
    2.63                     \<lambda>x. P(x) <-> P'(x), 
    2.64                     \<lambda>a x. Q(a,x) <-> Q'(a,x))"
    2.65  by (simp add: Reflects_def Closed_Unbounded_Int, blast) 
    2.66 @@ -155,7 +155,7 @@
    2.67  
    2.68  lemma (in ex_reflection) ClEx_upward:
    2.69       "[| z\<in>Mset(a); y\<in>Mset(a); Q(a,<y,z>); Cl(a); ClEx(P,a) |] 
    2.70 -      ==> \<exists>z. M(z) \<and> P(<y,z>)"
    2.71 +      ==> \<exists>z. M(z) & P(<y,z>)"
    2.72  apply (simp add: ClEx_def M_def)
    2.73  apply (blast dest: Cl_reflects
    2.74  	     intro: Limit_is_Ord Pair_in_Mset)
    2.75 @@ -164,7 +164,7 @@
    2.76  text{*Class @{text ClEx} indeed consists of reflecting ordinals...*}
    2.77  lemma (in ex_reflection) ZF_ClEx_iff:
    2.78       "[| y\<in>Mset(a); Cl(a); ClEx(P,a) |] 
    2.79 -      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
    2.80 +      ==> (\<exists>z. M(z) & P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
    2.81  by (blast intro: dest: ClEx_downward ClEx_upward) 
    2.82  
    2.83  text{*...and it is closed and unbounded*}
    2.84 @@ -181,7 +181,7 @@
    2.85  lemma (in reflection) ClEx_iff:
    2.86       "[| y\<in>Mset(a); Cl(a); ClEx(P,a);
    2.87          !!a. [| Cl(a); Ord(a) |] ==> \<forall>x\<in>Mset(a). P(x) <-> Q(a,x) |] 
    2.88 -      ==> (\<exists>z. M(z) \<and> P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
    2.89 +      ==> (\<exists>z. M(z) & P(<y,z>)) <-> (\<exists>z\<in>Mset(a). Q(a,<y,z>))"
    2.90  apply (unfold ClEx_def FF_def F0_def M_def)
    2.91  apply (rule ex_reflection.ZF_ClEx_iff
    2.92    [OF ex_reflection.intro, OF reflection.intro ex_reflection_axioms.intro,
    2.93 @@ -209,8 +209,8 @@
    2.94  
    2.95  lemma (in reflection) Ex_reflection_0:
    2.96       "Reflects(Cl,P0,Q0) 
    2.97 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(P0,a), 
    2.98 -                   \<lambda>x. \<exists>z. M(z) \<and> P0(<x,z>), 
    2.99 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(P0,a), 
   2.100 +                   \<lambda>x. \<exists>z. M(z) & P0(<x,z>), 
   2.101                     \<lambda>a x. \<exists>z\<in>Mset(a). Q0(a,<x,z>))" 
   2.102  apply (simp add: Reflects_def) 
   2.103  apply (intro conjI Closed_Unbounded_Int)
   2.104 @@ -221,7 +221,7 @@
   2.105  
   2.106  lemma (in reflection) All_reflection_0:
   2.107       "Reflects(Cl,P0,Q0) 
   2.108 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x.~P0(x), a), 
   2.109 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x.~P0(x), a), 
   2.110                     \<lambda>x. \<forall>z. M(z) --> P0(<x,z>), 
   2.111                     \<lambda>a x. \<forall>z\<in>Mset(a). Q0(a,<x,z>))" 
   2.112  apply (simp only: all_iff_not_ex_not ball_iff_not_bex_not) 
   2.113 @@ -231,15 +231,15 @@
   2.114  
   2.115  theorem (in reflection) Ex_reflection [intro]:
   2.116       "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   2.117 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   2.118 -                   \<lambda>x. \<exists>z. M(z) \<and> P(x,z), 
   2.119 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   2.120 +                   \<lambda>x. \<exists>z. M(z) & P(x,z), 
   2.121                     \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
   2.122  by (rule Ex_reflection_0 [of _ " \<lambda>x. P(fst(x),snd(x))" 
   2.123                                 "\<lambda>a x. Q(a,fst(x),snd(x))", simplified])
   2.124  
   2.125  theorem (in reflection) All_reflection [intro]:
   2.126       "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   2.127 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   2.128 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   2.129                     \<lambda>x. \<forall>z. M(z) --> P(x,z), 
   2.130                     \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
   2.131  by (rule All_reflection_0 [of _ "\<lambda>x. P(fst(x),snd(x))" 
   2.132 @@ -249,14 +249,14 @@
   2.133  
   2.134  theorem (in reflection) Rex_reflection [intro]:
   2.135       "Reflects(Cl, \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))) 
   2.136 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   2.137 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. P(fst(x),snd(x)), a), 
   2.138                     \<lambda>x. \<exists>z[M]. P(x,z), 
   2.139                     \<lambda>a x. \<exists>z\<in>Mset(a). Q(a,x,z))"
   2.140  by (unfold rex_def, blast) 
   2.141  
   2.142  theorem (in reflection) Rall_reflection [intro]:
   2.143       "Reflects(Cl,  \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x)))
   2.144 -      ==> Reflects(\<lambda>a. Cl(a) \<and> ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   2.145 +      ==> Reflects(\<lambda>a. Cl(a) & ClEx(\<lambda>x. ~P(fst(x),snd(x)), a), 
   2.146                     \<lambda>x. \<forall>z[M]. P(x,z), 
   2.147                     \<lambda>a x. \<forall>z\<in>Mset(a). Q(a,x,z))" 
   2.148  by (unfold rall_def, blast) 
   2.149 @@ -272,7 +272,7 @@
   2.150  proof state.*}
   2.151  lemma (in reflection) 
   2.152       "Reflects(?Cl,
   2.153 -               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   2.154 +               \<lambda>x. \<exists>y. M(y) & x \<in> y, 
   2.155                 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)"
   2.156  by fast
   2.157  
   2.158 @@ -280,8 +280,8 @@
   2.159  in the class of reflecting ordinals.  The @{term "Ord(a)"} is redundant,
   2.160  though harmless.*}
   2.161  lemma (in reflection) 
   2.162 -     "Reflects(\<lambda>a. Ord(a) \<and> ClEx(\<lambda>x. fst(x) \<in> snd(x), a),   
   2.163 -               \<lambda>x. \<exists>y. M(y) \<and> x \<in> y, 
   2.164 +     "Reflects(\<lambda>a. Ord(a) & ClEx(\<lambda>x. fst(x) \<in> snd(x), a),   
   2.165 +               \<lambda>x. \<exists>y. M(y) & x \<in> y, 
   2.166                 \<lambda>a x. \<exists>y\<in>Mset(a). x \<in> y)" 
   2.167  by fast
   2.168  
   2.169 @@ -289,31 +289,31 @@
   2.170  text{*Example 2*}
   2.171  lemma (in reflection) 
   2.172       "Reflects(?Cl,
   2.173 -               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.174 +               \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.175                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   2.176  by fast
   2.177  
   2.178  text{*Example 2'.  We give the reflecting class explicitly. *}
   2.179  lemma (in reflection) 
   2.180    "Reflects
   2.181 -    (\<lambda>a. (Ord(a) \<and>
   2.182 -          ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) \<and>
   2.183 +    (\<lambda>a. (Ord(a) &
   2.184 +          ClEx(\<lambda>x. ~ (snd(x) \<subseteq> fst(fst(x)) --> snd(x) \<in> snd(fst(x))), a)) &
   2.185            ClEx(\<lambda>x. \<forall>z. M(z) --> z \<subseteq> fst(x) --> z \<in> snd(x), a),
   2.186 -	    \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.187 +	    \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.188  	    \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   2.189  by fast
   2.190  
   2.191  text{*Example 2''.  We expand the subset relation.*}
   2.192  lemma (in reflection) 
   2.193    "Reflects(?Cl,
   2.194 -        \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
   2.195 +        \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> (\<forall>w. M(w) --> w\<in>z --> w\<in>x) --> z\<in>y),
   2.196          \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). (\<forall>w\<in>Mset(a). w\<in>z --> w\<in>x) --> z\<in>y)"
   2.197  by fast
   2.198  
   2.199  text{*Example 2'''.  Single-step version, to reveal the reflecting class.*}
   2.200  lemma (in reflection) 
   2.201       "Reflects(?Cl,
   2.202 -               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.203 +               \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<subseteq> x --> z \<in> y), 
   2.204                 \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<subseteq> x --> z \<in> y)" 
   2.205  apply (rule Ex_reflection) 
   2.206  txt{*
   2.207 @@ -333,21 +333,21 @@
   2.208  if @{term P} is quantifier-free, since it is not being relativized.*}
   2.209  lemma (in reflection) 
   2.210       "Reflects(?Cl,
   2.211 -               \<lambda>x. \<exists>y. M(y) \<and> (\<forall>z. M(z) --> z \<in> y <-> z \<in> x \<and> P(z)), 
   2.212 -               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x \<and> P(z))"
   2.213 +               \<lambda>x. \<exists>y. M(y) & (\<forall>z. M(z) --> z \<in> y <-> z \<in> x & P(z)), 
   2.214 +               \<lambda>a x. \<exists>y\<in>Mset(a). \<forall>z\<in>Mset(a). z \<in> y <-> z \<in> x & P(z))"
   2.215  by fast
   2.216  
   2.217  text{*Example 3'*}
   2.218  lemma (in reflection) 
   2.219       "Reflects(?Cl,
   2.220 -               \<lambda>x. \<exists>y. M(y) \<and> y = Collect(x,P),
   2.221 +               \<lambda>x. \<exists>y. M(y) & y = Collect(x,P),
   2.222                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Collect(x,P))";
   2.223  by fast
   2.224  
   2.225  text{*Example 3''*}
   2.226  lemma (in reflection) 
   2.227       "Reflects(?Cl,
   2.228 -               \<lambda>x. \<exists>y. M(y) \<and> y = Replace(x,P),
   2.229 +               \<lambda>x. \<exists>y. M(y) & y = Replace(x,P),
   2.230                 \<lambda>a x. \<exists>y\<in>Mset(a). y = Replace(x,P))";
   2.231  by fast
   2.232  
   2.233 @@ -355,7 +355,7 @@
   2.234  to be relativized.*}
   2.235  lemma (in reflection) 
   2.236       "Reflects(?Cl,
   2.237 -               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) \<and> f \<in> (\<Pi>X \<in> A. X)),
   2.238 +               \<lambda>A. 0\<notin>A --> (\<exists>f. M(f) & f \<in> (\<Pi>X \<in> A. X)),
   2.239                 \<lambda>a A. 0\<notin>A --> (\<exists>f\<in>Mset(a). f \<in> (\<Pi>X \<in> A. X)))"
   2.240  by fast
   2.241  
     3.1 --- a/src/ZF/Constructible/Relative.thy	Mon Sep 09 17:28:29 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Sep 10 16:47:17 2002 +0200
     3.3 @@ -244,13 +244,15 @@
     3.4  	\<forall>x[M]. \<forall>y[M]. (\<forall>z[M]. z \<in> x <-> z \<in> y) --> x=y"
     3.5  
     3.6    separation :: "[i=>o, i=>o] => o"
     3.7 -    --{*Big problem: the formula @{text P} should only involve parameters
     3.8 -        belonging to @{text M}.  Don't see how to enforce that.*}
     3.9 +    --{*The formula @{text P} should only involve parameters
    3.10 +        belonging to @{text M}.  But we can't prove separation as a scheme
    3.11 +        anyway.  Every instance that we need must individually be assumed
    3.12 +        and later proved.*}
    3.13      "separation(M,P) == 
    3.14  	\<forall>z[M]. \<exists>y[M]. \<forall>x[M]. x \<in> y <-> x \<in> z & P(x)"
    3.15  
    3.16    upair_ax :: "(i=>o) => o"
    3.17 -    "upair_ax(M) == \<forall>x y. M(x) --> M(y) --> (\<exists>z[M]. upair(M,x,y,z))"
    3.18 +    "upair_ax(M) == \<forall>x[M]. \<forall>y[M]. \<exists>z[M]. upair(M,x,y,z)"
    3.19  
    3.20    Union_ax :: "(i=>o) => o"
    3.21      "Union_ax(M) == \<forall>x[M]. \<exists>z[M]. big_union(M,x,z)"
    3.22 @@ -260,7 +262,7 @@
    3.23  
    3.24    univalent :: "[i=>o, i, [i,i]=>o] => o"
    3.25      "univalent(M,A,P) == 
    3.26 -	(\<forall>x[M]. x\<in>A --> (\<forall>y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))"
    3.27 +	(\<forall>x[M]. x\<in>A --> (\<forall>y[M]. \<forall>z[M]. P(x,y) & P(x,z) --> y=z))"
    3.28  
    3.29    replacement :: "[i=>o, [i,i]=>o] => o"
    3.30      "replacement(M,P) == 
    3.31 @@ -274,7 +276,7 @@
    3.32  
    3.33    foundation_ax :: "(i=>o) => o"
    3.34      "foundation_ax(M) == 
    3.35 -	\<forall>x[M]. (\<exists>y\<in>x. M(y)) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
    3.36 +	\<forall>x[M]. (\<exists>y[M]. y\<in>x) --> (\<exists>y[M]. y\<in>x & ~(\<exists>z[M]. z\<in>x & z \<in> y))"
    3.37  
    3.38  
    3.39  subsection{*A trivial consistency proof for $V_\omega$ *}