# Inner Models

Require Export ST.

(* An inner model is a class of sets satisfying the axioms of set theory *)

Section Sub.

Variable set : SetStruct.
Variable p : set -> Prop.

Structure ZF_closed :=
{
p_trans : forall x y, y el x -> p x -> p y;
p_eset : p 0;
p_union : forall x, p x -> p (union x);
p_power : forall x, p x -> p (power x);
p_rep : forall R x, functional R ->
(forall y z, R y z -> y el x -> p z) ->
p x -> p (rep R x);
}.

Variable set_ZF : ZF set.
Variable PC : ZF_closed.

(* We define the substructure corresponding to p and show that it is a model *)

Definition P :=
{ x | p x }.

Fact PI x :
forall (PX PX' : p x), PX = PX'.
Proof.
apply proof_irrelevance.
Qed.

Definition embed R x y :=
exists (PX : p x) (PY : p y), R (exist p x PX) (exist p y PY).

Definition res (R : set -> set -> Prop) (X Y : P) :=
R (proj1_sig X) (proj1_sig Y).

Fact embed_fun R :
functional R -> functional (embed R).
Proof.
intros H x y y' [H1[H2 H3]] [I1[I2 I3]]. rewrite (PI H1 I1) in *.
specialize (H (exist p x I1) (exist p y H2) (exist p y' I2) H3 I3).
now apply EqdepFacts.eq_sig_fst in H.
Qed.

Fact res_fun R :
functional R -> functional (res R).
Proof.
intros FR [x PX] [y PY] [z PZ] H1 H2.
unfold res in *; simpl in *.
specialize (FR x y z H1 H2); subst.
now rewrite (PI PY PZ).
Qed.

Definition pseudo_rep R x :=
union (sing (rep (embed R) x) ! (fun _ => functional R)).

Fact pseudo_rep_fun R x :
functional R -> pseudo_rep R x = rep (embed R) x.
Proof.
intros H. unfold pseudo_rep.
now rewrite sep_true, sing_union.
Qed.

Fact pseudo_rep_neg R x :
~ functional R -> pseudo_rep R x = 0.
Proof.
intros H. unfold pseudo_rep.
now rewrite sep_false, union_eset.
Qed.

Definition IM : SetStruct.
apply (Build_SetStruct) with (set:=P).
- intros [x _] [y _]. exact (x el y).
- exists 0. now apply p_eset.
- intros [x XP]. exists (union x). now apply p_union.
- intros [x XP]. exists (power x). now apply p_power.
- intros R [x XP]. exists (pseudo_rep R x).
destruct (classic (functional R)).
+ rewrite pseudo_rep_fun; trivial.
apply p_rep; trivial; try now apply embed_fun.
now intros y z [_[PZ _]].
+ rewrite pseudo_rep_neg; trivial.
now apply p_eset.
Defined.

Lemma IM_ZF :
ZF IM.
Proof.
split.
- intros [x PX] [y PY] H1 H2.
assert (H : x = y).
+ apply Ext; intros z H3.
* apply (H1 (exist p z (p_trans PC H3 PX)) H3).
* apply (H2 (exist p z (p_trans PC H3 PY)) H3).
+ subst y. rewrite (PI PY PX). reflexivity.
- intros [x PX] H. apply (Eset (z:=x)), H.
- intros [x PX] [y PY]. split; intros H.
+ apply (Union x y) in H as [z[Z1 Z2]].
now exists (exist p z (p_trans PC Z1 PX)).
+ apply (Union x y). destruct H as [[z PZ] Z]. now exists z.
- intros [x PX] [y PY]. split; intros H.
+ apply (Power x y) in H. intros [z PZ] Z. apply H, Z.
+ apply (Power x y). intros z Z.
apply (H (exist p z (p_trans PC Z PY)) Z).
- intros R FR [x PX] [y PY]. split; intros H.
+ apply Union in H. rewrite sep_true in H; trivial.
apply Union in H. rewrite sing_union in H.
apply Rep in H as [z[Z[H1[H2 H3]]]]; try now apply embed_fun.
exists (exist p z (p_trans PC Z PX)).
rewrite (PI (p_trans PC Z PX) H1), (PI PY H2). now split.
+ apply Union. rewrite sep_true; trivial.
apply Union. rewrite sing_union.
destruct H as [[z PZ][Z1 Z2]].
apply Rep; try now apply embed_fun. exists z.
split; trivial. now exists PZ, PY.
- intros [x PX]. induction (AxWF x) as [x _ IH].
constructor. intros [y PY] Y. now apply IH.
Qed.

End Sub.