Shrinking Lemma

Require Export Embeddings Stage.

ZF-closed classes induce submodels of ZF

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'.
    apply proof_irrelevance.

  Lemma P_eq x y (PX : p x) (PY : p y) :
    toP PX = toP PY <-> x = y.
    split; intros H.
    - change (proj1_sig (toP PX) = proj1_sig (toP PY)). now rewrite H.
    - subst. now rewrite (PI PX PY).

  Lemma P_proj X :
    toP (proj2_sig X) = X.
    destruct X. reflexivity.

  Definition PS : SetStruct.
    apply (@Build_SetStruct P).
    intros [x _] [y _]. exact (x el y).

  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.

  (* P is a model of Z *)

  Lemma P_Ext (x y : PS) :
    x == y <-> x = y.
    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).

  Lemma P_WF (x : PS) :
    WF x.
    destruct x as [x PX]. induction (PWF PX) as [x _ IH].
    constructor. intros [y PY] Y. now apply IH.

  Lemma fress F :
    fres equiv F.
    now intros a a' -> % ZFSExt.

  Lemma cress P :
    cres equiv P.
    now intros a a' -> % ZFSExt.

  Hint Resolve fress cress.

  Fact P_Z :
    Z PZ.
    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.

  (* Next we turn P into a ZF'-structure *)

  Lemma ZFSDesc (P : set -> Prop) x :
     P x -> unique P -> P (delta P).
    intros H1 H2. apply ZFSDesc1.
    exists x. intros y. rewrite ZFSExt.
    split; intros H.
    - now apply H2.
    - now rewrite H.

  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).
    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.

  Lemma embed_delta F x :
     p x -> embed F x (delta (embed F x)).
    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.

  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_]].

  (* 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.
    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.

  Fact P_ZF' :
    ZF' PZF'.
    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.

  (* 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.
    intros [x X]. split.
    - exists x. now apply X, P_Ext.
    - intros y y'. rewrite !X, !P_Ext. congruence.

  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.
    intros H. apply ZFSExt; split.
    - intros y [Y1 Y2] % Sep; trivial.
    - intros y Y. apply Sep; auto.

  Fact sep_false (x : set) (Q : set -> Prop) :
    (forall x, ~ Q x) -> sep Q x = 0.
    intros H. apply ZFSExt; split.
    - intros y [Y1 Y2] % Sep; trivial. contradiction (H y).
    - now intros y Y % Eset.

  Fact desc_issing q :
    issing q -> desc q = delta (emclass q).
    intros H. unfold desc.
    now rewrite sep_true.

  Fact desc_nissing q :
    ~ issing q -> desc q = 0.
    intros H. unfold desc.
    now rewrite sep_false.

  Lemma emc_issing q :
    issing q -> exists x, emclass q x /\ unique (emclass q).
    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.

  Lemma desc_p q :
    p (desc q).
    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.

  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'.
    intros [[x X] U] H. split.
    - exists x. now apply H.
    - intros y y'. rewrite <- !H. apply U.

  Lemma delta_equal (Q : set -> Prop) x :
    Q x -> unique Q -> delta Q = x.
    intros H1 H2. apply H2; trivial.
    now apply (ZFSDesc H1).

  Theorem IM_ZF :
    ZF IM.
    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').

End Sub.

Hint Resolve cress fress.

Models of strength n admit inner models of ZFn

Section IMISO.

  Context { M : ZFStruct }.
  Context { MZF : ZF M }.

  Variable p : M -> Prop.
  Hypothesis PC : closed_ZF p.

  Lemma ZF_ZFS :
    ZFS M.
    split; try apply HiZF.
    - apply ZFExt.
    - apply Desc1.
    - apply Desc2.

  Definition MP :=

  Definition exmp x (PX : p x) : MP :=
    exist _ x PX.

  Instance MPZF :
    ZF MP.
    apply IM_ZF. apply WF_sub.

  Definition pi (x : MP) : M :=
    proj1_sig x.

  Lemma pi_mor (x y : MP) :
    x el y <-> pi x el pi y.
    now destruct x, y; simpl.

  Lemma pi_sur (x : MP) (y' : M) :
    y' el pi x -> exists y, y el x /\ pi y == y'.
    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.

  Lemma IM_universe u (PU : p u) :
    universe u <-> universe (exmp PU).
    rewrite (h_universe (h:=pi)).
    - simpl. reflexivity.
    - apply pi_mor.
    - apply pi_sur.

  Lemma IM_strength x n (PX : p x) :
     strength n x <-> strength n (exmp PX).
    rewrite (h_strength (h:=pi)).
    - simpl. reflexivity.
    - apply pi_mor.
    - apply pi_sur.


Lemma shrink n :
  (exists M, ZFge n M) -> (exists M, ZFn n M).
  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.