Large Models


Require Export Quotient_TD.

Embedding of intensional models yields universes


Section Embed.

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

  Definition ST (x : M) :=
    sig (fun y => y el x).

  Fixpoint em' (x : M) (T : WF x) : ACZ :=
    let (F) := T in Asup (ST x) (fun p => let (y, Y) := p in em' (F y Y)).

  Definition em (x : M) : ACZ :=
    em' (AxWF x).

  Definition U : ACZ :=
    Asup M em.

  Lemma em_invar (x : M) (T1 T2 : WF x) :
    Aeq (em' T1) (em' T2).
  Proof.
    revert T1 T2. induction (AxWF x) as [x _ IH].
    intros [F1] [F2]. split.
    - intros [y H]. exists (exist _ y H). now apply IH.
    - intros [y H]. exists (exist _ y H). now apply IH.
  Qed.

  Lemma em_rec x :
    Aeq (em x) (Asup (ST x) (fun p => let (y, _) := p in em y)).
  Proof.
    unfold em. destruct (AxWF) as [F]. split.
    - intros [y Y]. exists (exist _ y Y). apply em_invar.
    - intros [y Y]. exists (exist _ y Y). apply em_invar.
  Qed.

  Lemma equiv_em x y :
    x == y -> Aeq (em x) (em y).
  Proof.
    intros H. rewrite !em_rec.
    apply Aeq_ext; intros s [[z Z1] Z2].
    - rewrite H in Z1. now exists (exist _ z Z1).
    - rewrite <- H in Z1. now exists (exist _ z Z1).
  Qed.

  Lemma em_equiv x y :
    Aeq (em x) (em y) -> x == y.
  Proof.
    revert y. induction (AxWF x) as [x _ IH].
    intros y. repeat rewrite em_rec.
    intros [H1 H2]. split; intros z Z.
    - destruct (H1 (exist _ z Z)) as [[z' Z1] Z2].
      now rewrite (IH z Z z').
    - destruct (H2 (exist _ z Z)) as [[z' Z1] Z2].
      now rewrite <- (IH z' Z1 z).
  Qed.

  Lemma em_mor x y :
    x el y <-> em x el em y.
  Proof.
    split; intros H.
    - simpl. rewrite (em_rec y).
      now exists (exist _ x H).
    - rewrite (em_rec y) in H. destruct H as [[x' H1]H2].
      apply em_equiv in H2. now rewrite H2.
  Qed.

  Lemma em_sur x s :
    s el em x -> exists y, y el x /\ em y == s.
  Proof.
    rewrite em_rec. intros [[y X] Y].
    exists y. split; trivial. now apply Aeq_equiv.
  Qed.

  Theorem U_universe :
    universe U.
  Proof.
    unfold universe.
    apply (h_const em_mor em_sur).
    intros s. split.
    - intros [x H]. exists x. unfold const.
      split; auto. now apply Aeq_equiv.
    - intros [x[X _]]. exists x. now apply Aeq_equiv.
  Qed.

  Fact trans_strength n (x : ACZ) :
  trans x -> (exists y, y el x /\ strength n y) -> strength n x.
  Proof.
    destruct n; cbn; auto.
    intros H1 [y[H2 [u[U1[U2 U3]]]]].
    exists u. split; try now apply (H1 y). now split.
  Qed.

  Fact U_strength n :
    (exists (X : M), strength n X) -> strength n U.
  Proof.
    intros [X HX]. apply trans_strength.
    - apply U_universe.
    - exists (em X). split.
      + now exists X.
      + now apply (h_strength em_mor em_sur).
  Qed.

End Embed.

Consistency of ZF>=n


(* If a model of strength n exists then a model of strength n+1 exists *)

Lemma uni_strength n (u : SET) :
  universe u -> strength n u -> (exists (x : SET), strength (S n) x).
Proof.
  intros U1 U2. exists (power u), u. split; auto.
  apply Power. intros x. tauto.
Qed.

Theorem step n :
  (exists M, ZFge n M) -> (exists M, ZFge (S n) M).
Proof.
  intros [M[M1 M2]]. exists SET. split; trivial.
  apply (@uni_strength n (ATS U)).
  - apply ATS_universe, U_universe.
  - now apply ATS_strength, U_strength.
Qed.

(* Thus we can construct models of arbitrary finite strength.
   In ZFge_cons any number can be entered. *)


Lemma ZFge0 M :
  ZF M -> ZFge 0 M.
Proof.
  intros H. split; trivial.
  simpl. now exists 0.
Qed.

Fact ZFge_cons :
  exists M, ZFge 3 M.
Proof.
  repeat apply step.
  exists SET. now apply ZFge0.
Qed.

(* However, because of non-dependent type universes the universal closure is not provable. *)

Set Printing Universes.

Fact ZFn_cons_not_provable n :
  exists M, ZFge n M.
Proof.
  induction n.
  - exists SET. now apply ZFge0.
  - apply step. try apply IHn.
Admitted.

Unset Printing Universes.

(* In fact the universal closure for non-dependent universe levels would imply a model of ZFw. *)

Fact ZFn_ZFw :
  (forall n, exists M, ZFge n M) -> (exists M, ZFw M).
Proof.
  intros H. exists SET. split; trivial.
  intros n. destruct (H n) as [M [H1 H2]].
  exists (ATS U). now apply ATS_strength, U_strength.
Qed.