Section Sub.
Variable set : ZFStruct.
Variable p : set -> Prop.
Hypothesis set_ZF : ZFS set.
Hypothesis PC : closed_ZF p.
Hypothesis PWF : p <=p WF.
(* We first turn the class P into a Z-structure *)
Definition P :=
{ x | p x }.
Definition toP x PX :=
exist p x PX.
Fact PI x :
forall (PX PX' : p x), PX = PX'.
Proof.
apply proof_irrelevance.
Qed.
Lemma P_eq x y (PX : p x) (PY : p y) :
toP PX = toP PY <-> x = y.
Proof.
split; intros H.
- change (proj1_sig (toP PX) = proj1_sig (toP PY)). now rewrite H.
- subst. now rewrite (PI PX PY).
Qed.
Lemma P_proj X :
toP (proj2_sig X) = X.
Proof.
destruct X. reflexivity.
Qed.
Definition PS : SetStruct.
apply (@Build_SetStruct P).
intros [x _] [y _]. exact (x el y).
Defined.
Definition emclass (q : P -> Prop) x :=
exists (PX : p x), q (toP PX).
Definition PZ : ZStruct.
apply (@Build_ZStruct PS).
- exists 0. apply PC.
- intros [x X] [y Y]. exists (upair x y). now apply PC.
- intros [x X]. exists (union x). now apply PC.
- intros [x X]. exists (power x). now apply PC.
- intros q [x X]. exists (sep (emclass q) x).
apply PC; trivial. now intros a a' -> % ZFSExt.
Defined.
(* P is a model of Z *)
Lemma P_Ext (x y : PS) :
x == y <-> x = y.
Proof.
split; try now intros ->.
destruct x as [x PX], y as [y PY]. intros [H1 H2].
apply P_eq. apply ZFSExt; split; intros z H3.
- apply (H1 (exist p z (U_trans PC PX H3)) H3).
- apply (H2 (exist p z (U_trans PC PY H3)) H3).
Qed.
Lemma P_WF (x : PS) :
WF x.
Proof.
destruct x as [x PX]. induction (PWF PX) as [x _ IH].
constructor. intros [y PY] Y. now apply IH.
Qed.
Lemma fress F :
fres equiv F.
Proof.
now intros a a' -> % ZFSExt.
Qed.
Lemma cress P :
cres equiv P.
Proof.
now intros a a' -> % ZFSExt.
Qed.
Hint Resolve fress cress.
Fact P_Z :
Z PZ.
Proof.
split; try apply P_Ext.
split; try apply P_WF. split.
- now intros x x' y -> % P_Ext.
- intros [x PX] H. apply (Eset (z:=x)), H.
- intros [x PX] [y PY] [z PZ].
now rewrite (Pair x y z), !P_Ext, !ZFSExt, !P_eq.
- intros [x PX] [y PY]. rewrite (Union x y). split; intros H.
+ destruct H as [z[Z1 Z2]]. now exists (exist p z (U_trans PC PX Z1)).
+ destruct H as [[z PZ] Z]. now exists z.
- intros [x PX] [y PY]. rewrite (Power x y). split; intros H.
+ intros [z PZ] Z. apply H, Z.
+ intros z Z. apply (H (exist p z (U_trans PC PY Z)) Z).
- intros q [x PX] [y PY] _. split; intros H.
+ apply (Sep (P:=emclass q)) in H as [H1 [PY' H2]]; trivial.
split; trivial. now rewrite (PI PY PY').
+ apply (Sep (P:=emclass q)); trivial. destruct H as [H1 H2].
split; trivial. now exists PY.
Qed.
(* Next we turn P into a ZF'-structure *)
Lemma ZFSDesc (P : set -> Prop) x :
P x -> unique P -> P (delta P).
Proof.
intros H1 H2. apply ZFSDesc1.
exists x. intros y. rewrite ZFSExt.
split; intros H.
- now apply H2.
- now rewrite H.
Qed.
Definition embed F x y :=
exists (PX : p x) (PY : p y), (toP PY) = F (toP PX).
Lemma embed_unique F x :
unique (embed F x).
Proof.
intros y y' [PX[PY H1]] [PX'[PY' H2]].
rewrite (PI PX' PX) in H2. rewrite <- H2 in H1.
now apply P_eq in H1.
Qed.
Lemma embed_delta F x :
p x -> embed F x (delta (embed F x)).
Proof.
intros H.
pose (z := proj1_sig (F (toP H))).
pose (PZ := proj2_sig (F (toP H))).
eapply ZFSDesc; try apply embed_unique.
exists H, PZ. rewrite <- P_proj. reflexivity.
Qed.
Definition rep' F x :=
frep (fun y => delta (embed F y)) (sep p x).
Definition PZF' : ZFStruct'.
apply (@Build_ZFStruct' PZ).
intros F [x X]. exists (rep' F x).
repeat apply PC; trivial.
intros z [y[H -> % ZFSExt]] % ZFSFrep; trivial.
apply Sep in H as [H1 H2]; trivial.
now apply (@embed_delta F) in H2 as [PY[PZ_]].
Defined.
(* We prove that P is a model of ZF' *)
Lemma ax_rep' F x z :
z el rep' F x <-> exists y, y el x /\ embed F y z.
Proof.
unfold rep'. rewrite ZFSFrep; trivial.
split; intros [y[Y1 Y2]]; exists y; split.
- now apply Sep in Y1.
- apply ZFSExt in Y2. subst z. apply Sep in Y1; trivial. now apply embed_delta.
- destruct Y2 as [PY _]. apply Sep; trivial. now split.
- apply ZFSExt. apply (embed_unique Y2).
apply (ZFSDesc Y2), embed_unique.
Qed.
Fact P_ZF' :
ZF' PZF'.
Proof.
split; try apply P_Ext.
split; try apply P_Z.
intros F [x PX] [z PZ] _. rewrite (ax_rep' F x z).
split; intros H.
- destruct H as [y[Y1 [PY[PZ' Y2]]]].
exists (toP PY). split; trivial.
now rewrite P_Ext, (PI PZ PZ').
- destruct H as [[y PY][Y1 Y2 % P_Ext]].
exists y. split; trivial. now exists PY, PZ.
Qed.
(* We finally define a description operator for P *)
Definition issing (q : PS -> Prop) :=
ex q /\ unique q.
Lemma sing_eqcl q :
iseqcl q -> issing q.
Proof.
intros [x X]. split.
- exists x. now apply X, P_Ext.
- intros y y'. rewrite !X, !P_Ext. congruence.
Qed.
Definition desc (q : P -> Prop) :=
sep (fun _ => issing q) (delta (emclass q)).
Fact sep_true (x : set) (Q : set -> Prop) :
(forall x, Q x) -> sep Q x = x.
Proof.
intros H. apply ZFSExt; split.
- intros y [Y1 Y2] % Sep; trivial.
- intros y Y. apply Sep; auto.
Qed.
Fact sep_false (x : set) (Q : set -> Prop) :
(forall x, ~ Q x) -> sep Q x = 0.
Proof.
intros H. apply ZFSExt; split.
- intros y [Y1 Y2] % Sep; trivial. contradiction (H y).
- now intros y Y % Eset.
Qed.
Fact desc_issing q :
issing q -> desc q = delta (emclass q).
Proof.
intros H. unfold desc.
now rewrite sep_true.
Qed.
Fact desc_nissing q :
~ issing q -> desc q = 0.
Proof.
intros H. unfold desc.
now rewrite sep_false.
Qed.
Lemma emc_issing q :
issing q -> exists x, emclass q x /\ unique (emclass q).
Proof.
intros [[x X] H]. exists (proj1_sig x). split.
- exists (proj2_sig x). now rewrite P_proj.
- intros a b [A1 A2] [B1 B2].
apply (@P_eq a b A1 B1). now apply H.
Qed.
Lemma desc_p q :
p (desc q).
Proof.
destruct (classic (issing q)) as [H|H].
- rewrite desc_issing; trivial.
destruct (emc_issing H) as [x[X1 X2]].
rewrite (X2 (delta (emclass q)) x); trivial.
+ now destruct X1.
+ now apply (ZFSDesc X1).
- rewrite desc_nissing; trivial. apply PC.
Qed.
Definition descp q :=
toP (desc_p q).
Definition IM :=
@Build_ZFStruct PZF' descp.
(* The main result is that P is a model of ZF *)
Lemma issing_ext q q' :
issing q -> (forall x : IM, q x <-> q' x) -> issing q'.
Proof.
intros [[x X] U] H. split.
- exists x. now apply H.
- intros y y'. rewrite <- !H. apply U.
Qed.
Lemma delta_equal (Q : set -> Prop) x :
Q x -> unique Q -> delta Q = x.
Proof.
intros H1 H2. apply H2; trivial.
now apply (ZFSDesc H1).
Qed.
Theorem IM_ZF :
ZF IM.
Proof.
split; try apply P_Ext.
split; try apply P_ZF'.
- intros q QE % sing_eqcl. simpl.
cut (emclass q (delta (emclass q))).
+ intros [H1 H2]. unfold descp.
destruct (P_eq H1 (desc_p q)) as [_ <-]; trivial.
symmetry. now apply desc_issing.
+ destruct (emc_issing QE) as [x[X1 X2]].
now apply (ZFSDesc X1).
- intros q q' E. apply P_eq.
destruct (classic (issing q)) as [H|H];
destruct (classic (issing q')) as [H'|H'].
+ rewrite (desc_issing H), (desc_issing H').
apply emc_issing in H as [y[Y1 Y2]].
apply emc_issing in H' as [y'[Y1' Y2']].
rewrite (delta_equal Y1), (delta_equal Y1'); trivial.
apply Y2; trivial. destruct Y1' as [PY Y].
exists PY. now apply E.
+ contradict H'. now apply (issing_ext H).
+ contradict H. apply (issing_ext H'). intros x. now rewrite E.
+ now rewrite (desc_nissing H), (desc_nissing H').
Qed.
End Sub.
Hint Resolve cress fress.
Section IMISO.
Context { M : ZFStruct }.
Context { MZF : ZF M }.
Variable p : M -> Prop.
Hypothesis PC : closed_ZF p.
Lemma ZF_ZFS :
ZFS M.
Proof.
split; try apply HiZF.
- apply ZFExt.
- apply Desc1.
- apply Desc2.
Qed.
Definition MP :=
IM ZF_ZFS PC.
Definition exmp x (PX : p x) : MP :=
exist _ x PX.
Instance MPZF :
ZF MP.
Proof.
apply IM_ZF. apply WF_sub.
Qed.
Definition pi (x : MP) : M :=
proj1_sig x.
Lemma pi_mor (x y : MP) :
x el y <-> pi x el pi y.
Proof.
now destruct x, y; simpl.
Qed.
Lemma pi_sur (x : MP) (y' : M) :
y' el pi x -> exists y, y el x /\ pi y == y'.
Proof.
destruct x as [x' X]. intros H; simpl in H.
assert (Y : p y') by now apply (U_trans PC X).
exists (toP Y). simpl. split; trivial. reflexivity.
Qed.
Lemma IM_universe u (PU : p u) :
universe u <-> universe (exmp PU).
Proof.
rewrite (h_universe (h:=pi)).
- simpl. reflexivity.
- apply pi_mor.
- apply pi_sur.
Qed.
Lemma IM_strength x n (PX : p x) :
strength n x <-> strength n (exmp PX).
Proof.
rewrite (h_strength (h:=pi)).
- simpl. reflexivity.
- apply pi_mor.
- apply pi_sur.
Qed.
End IMISO.
Lemma shrink n :
(exists M, ZFge n M) -> (exists M, ZFn n M).
Proof.
intros [M[MZF[X XN]]].
destruct (classic (exists X', strength (S n) X')) as [[X'[U'[U1' U2']]]|H].
- apply universe_least in U2' as [U[[U1 U2] U3]].
clear U1' U' X'. exists (IM ZF_ZFS U1). split.
+ split; try apply IM_ZF, WF_sub.
apply (uni_strength U1) in U2 as [U'[H1 H2]].
exists (exmp U1 H1). now apply IM_strength.
+ intros [[X' H] [U'[H1 H2]] % IM_strength].
apply (WF_no_loop (x:=U')). apply U3; trivial.
now apply (universe_trans U1 H).
- exists M. split; trivial. split; trivial. now exists X.
Qed.