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