(* WF is ZF-closed. *)
Section WF.
Context { M : ZFStruct }.
Context { MZFS : ZFS M }.
Lemma WF_trans :
ctrans WF.
Proof.
intros x y [H1] H2. now apply H1.
Qed.
Lemma WF_swelled :
cswelled WF.
Proof.
intros x y [H1] H2. constructor. auto.
Qed.
Lemma WF_eset :
WF 0.
Proof.
constructor. auto.
Qed.
Lemma WF_upair :
closed_upair WF.
Proof.
intros x y H1 H2. constructor.
intros z [Z|Z] % Pair; now apply ZFSExt in Z as ->.
Qed.
Lemma WF_union :
closed_union WF.
Proof.
intros x [H]. constructor.
intros y [z[H1 H2]] % Union.
now apply (H z H1).
Qed.
Lemma WF_power :
closed_power WF.
Proof.
intros x H. constructor.
intros y Y % Power.
now apply (WF_swelled H).
Qed.
Lemma WF_sep :
closed_sep WF.
Proof.
intros P x _ H. apply (WF_swelled H).
intros y [H1 H2] % Sep; eauto.
Qed.
Lemma WF_frep :
closed_frep WF.
Proof.
intros F x _ [H1] H2. now constructor.
Qed.
Lemma WF_Z :
closed_Z WF.
Proof.
split.
- apply WF_trans.
- apply WF_eset.
- apply WF_upair.
- apply WF_union.
- apply WF_power.
- apply WF_sep.
Qed.
Lemma WF_ZF :
closed_ZF WF.
Proof.
split.
- apply WF_Z.
- apply WF_frep.
Qed.
Theorem WF_model :
ZF (IM MZFS WF_ZF).
Proof.
now apply IM_ZF.
Qed.
End WF.
(* Every permutation of a model of ZF induces a model of ZF* *)
Section Perm.
Context { M : ZFStruct }.
Context { MZF : ZF M }.
Variable F G : M -> M.
Hypothesis FG :
forall x, F (G x) = x.
Hypothesis GF :
forall x, G (F x) = x.
Definition ele x y :=
x el (F y).
Definition sub x y :=
forall z, ele z x -> ele z y.
Definition empty :=
G eset.
Definition pair x y :=
G (upair x y).
Definition uni x :=
G (union (frep F (F x))).
Definition pow x :=
G (frep G (power (F x))).
Definition sepa P x :=
G (sep P (F x)).
Definition frepl f x :=
G (frep f (F x)).
Definition M_SS :=
@Build_SetStruct M ele.
Definition M_ZS :=
@Build_ZStruct M_SS empty pair uni pow sepa.
Definition M_ZF' :=
@Build_ZFStruct' M_ZS frepl.
Definition M_ZF :=
@Build_ZFStruct M_ZF' delta.
Lemma extAx (x y : M_SS) :
equiv x y <-> x = y.
Proof.
split; try now intros ->.
intros [H1 H2]. rewrite <- (GF x), <- (GF y).
apply f_equal. apply Ext; auto.
Qed.
Lemma emptyAx x :
~ ele x empty.
Proof.
unfold ele, empty. rewrite FG. apply Eset.
Qed.
Lemma pairAx x y z :
ele z (pair x y) <-> z = x \/ z = y.
Proof.
unfold ele, pair. rewrite FG. apply pair_el.
Qed.
Lemma unionAx x y :
ele y (uni x) <-> exists z, ele z x /\ ele y z .
Proof.
unfold ele, uni. rewrite FG.
split; intros H.
- apply Union in H as [z'[Z1 Z2]].
apply frep_el in Z1 as [z[Z3 ->]].
now exists z.
- destruct H as [z[Z1 Z2]]. apply Union.
exists (F z). split; trivial. apply frep_el.
now exists z.
Qed.
Lemma powerAx x y :
ele y (pow x) <-> sub y x.
Proof.
unfold ele, pow. rewrite FG.
split; intros H.
- intros z Z. apply frep_el in H as [y'[Y ->]].
apply Power in Y. apply Y. now rewrite <- (FG y').
- apply frep_el. exists (F y). rewrite GF. split; trivial.
apply Power. apply H.
Qed.
Lemma sepAx P x y :
ele y (sepa P x) <-> ele y x /\ P y.
Proof.
unfold ele, sepa. now rewrite FG, sep_el.
Qed.
Lemma frepAx f x z :
ele z (frepl f x) <-> exists y, ele y x /\ z = f y.
Proof.
unfold ele, frepl. now rewrite FG, frep_el.
Qed.
Lemma FM_ZS :
iZS M_ZS.
Proof.
split.
- now intros x x' y -> % extAx.
- apply emptyAx.
- intros x y z. rewrite !extAx. apply pairAx.
- apply unionAx.
- apply powerAx.
- intros P x y _. apply sepAx.
Qed.
Theorem FM_ZFS :
ZFS M_ZF.
Proof.
split.
- apply FM_ZS.
- apply extAx.
- intros f x z _. rewrite frepAx.
split; intros [y Y]; exists y.
+ now rewrite extAx.
+ now rewrite <- extAx.
- simpl. intros P [x H].
apply Desc1. exists x. intros y.
now rewrite H, extAx, ZFExt.
- simpl. apply Desc2.
Qed.
End Perm.
(* The transposition of 0 and 1 induces a model with a quine set *)
Section Instance.
Context { M : ZFStruct }.
Context { MZF : ZF M }.
Notation "1" := (power 0).
Definition R x y :=
(x = 0 /\ y = 1) \/ (x = 1 /\ y = 0)
\/ (x <> 0 /\ x <> 1 /\ y <> 0 /\ y <> 1 /\ x = y).
Definition R' x y :=
R y x.
Lemma R_unique x :
unique (R x).
Proof.
intros y y' [E1|[E2|H1]] [E3|[E4|H2]]; intuition; congruence.
Qed.
Lemma R'_unique x :
unique (R' x).
Proof.
intros y y' [E1|[E2|H1]] [E3|[E4|H2]]; intuition; congruence.
Qed.
Hint Resolve R_unique R'_unique.
Definition F x :=
delta (R x).
Definition G x :=
delta (R' x).
Lemma F0 :
F 0 = 1.
Proof.
apply delta_eq; trivial. now left.
Qed.
Lemma F1 :
F 1 = 0.
Proof.
apply delta_eq; trivial. right. now left.
Qed.
Lemma G0 :
G 0 = 1.
Proof.
apply delta_eq; trivial. right. now left.
Qed.
Lemma G1 :
G 1 = 0.
Proof.
apply delta_eq; trivial. now left.
Qed.
Lemma Fneq x :
x <> 0 -> x <> 1 -> F x = x.
Proof.
intros H1 H2. apply delta_eq; trivial.
repeat right. now repeat split.
Qed.
Lemma Gneq x :
x <> 0 -> x <> 1 -> G x = x.
Proof.
intros H1 H2. apply delta_eq; trivial.
repeat right. now repeat split.
Qed.
Lemma FG x :
F (G x) = x.
Proof.
destruct (classic (x = 0)) as [->|H1].
- now rewrite G0, F1.
- destruct (classic (x = 1)) as [->|H2].
+ now rewrite G1, F0.
+ apply delta_eq; trivial.
repeat right. now rewrite Gneq.
Qed.
Lemma GF x :
G (F x) = x.
Proof.
destruct (classic (x = 0)) as [->|H1].
- now rewrite F0, G1.
- destruct (classic (x = 1)) as [->|H2].
+ now rewrite F1, G0.
+ apply delta_eq; trivial.
repeat right. now rewrite Fneq.
Qed.
Lemma ZFS_model :
ZFS (M_ZF F G).
Proof.
apply FM_ZFS.
- apply FG.
- apply GF.
Qed.
Theorem antifounded :
ele F 0 0.
Proof.
unfold ele. rewrite F0. now apply Power.
Qed.
Lemma quine x :
ele F x 0 -> x = 0.
Proof.
intros H. apply sub_eset.
apply Power. now rewrite <- F0.
Qed.
End Instance.