Library Continuum.L
Require Import Basic_Constructions.
Import VectorDef.VectorNotations.
Require Import Coq.Logic.Classical.
Section L.
Context (S : ZF_Model).
Import VectorDef.VectorNotations.
Require Import Coq.Logic.Classical.
Section L.
Context (S : ZF_Model).
Definition zf_structure_over (A : Class) : ZF_Structure :=
build_zf_structure A (fun x y ⇒ x ∈ y).
Notation Is_Definable_Over
A x :=
(∀ n (type : Env_Type n),
Is_Definable_In_Env
(S := zf_structure_over A)
(fun _ : type ⇒ x)).
Definition Formula_Over (A : Class) (n : nat) : Type :=
Formula (S := zf_structure_over A) n.
Program Definition Def (A : S) : S :=
`{ B ⊆ A | ∃ ϕ : Formula_Over A 1, ∀ x : A, eval ϕ [x] ↔ x ∈ B }.
Next Obligation.
Admitted.
Global Instance Def_is_definable :
Is_Definable Def.
Admitted.
Program Definition L_stage : ordinals → S :=
ordinal_recursion
(fun previous_stage ⇒ Def previous_stage)
(fun previous_stages ⇒ big_union previous_stages).
Definition L_as_class : Class :=
build_class (fun x ⇒ ∃ α, x ∈ L_stage α).
Global Instance L_as_class_is_definable :
Is_Definable L_as_class.
Admitted.
Definition L :=
zf_structure_over L_as_class.
Lemma L_is_transitive :
∀ (x y : S), x ∈ L_as_class → y ∈ x → y ∈ L_as_class.
Proof.
intros A x [α HA] Hx.
revert α A x HA Hx. refine (ordinal_induction _ _ _).
- intros α _ A x HA Hx.
assert (H : A ⊆ L_stage α). {
unfold L_stage in HA.
rewrite ordinal_recursion_on_successor in HA.
unfold Def in HA.
rewrite in_separation_iff in HA. destruct HA as [HA _].
rewrite in_power_set_iff in HA.
exact HA.
}
∃ α. apply H. assumption.
- intros λ is_limit IH A x A_in_stage_λ x_in_A.
eassert (A ∈ ⋃ α : λ, L_stage (element α)).
+ unfold L_stage in A_in_stage_λ.
rewrite (ordinal_recursion_on_limit) in A_in_stage_λ.
× exact A_in_stage_λ.
× assumption.
+ rewrite in_indexed_union_iff in H.
destruct H as [α H].
apply (IH α A x H x_in_A).
Qed.
Definition constants_of_term {A} {n} (t : Term (S := zf_structure_over A) n) :=
match t with
| const _ x ⇒ `{x}
| var _ ⇒ ∅
end.
Fixpoint constants_of {A} {n} (ϕ : Formula_Over A n) : S :=
match ϕ with
| exist ϕ ⇒ constants_of ϕ
| and ϕ ψ ⇒ constants_of ϕ ∪ constants_of ψ
| not ϕ ⇒ constants_of ϕ
| equal t1 t2 ⇒ constants_of_term t1 ∪ constants_of_term t2
| is_element t1 t2 ⇒ constants_of_term t1 ∪ constants_of_term t2
end.
Lemma constants_of_term_form_subset
{A n} (t : Term (S := zf_structure_over A) n) :
constants_of_term t ⊆ A.
Proof.
destruct t; cbn.
- intros x Hx. rewrite in_singleton_iff in Hx. subst x. exact _.
- intros x Hx. apply not_in_empty_set in Hx. contradiction.
Qed.
Lemma constants_form_subset {A n} (ϕ : Formula_Over A n) :
constants_of ϕ ⊆ A.
Proof.
induction ϕ; cbn.
- exact IHϕ.
- intros x Hx. rewrite in_union_iff in Hx. destruct Hx; auto.
- exact IHϕ.
- intros x Hx. rewrite in_union_iff in Hx.
destruct Hx; eapply (constants_of_term_form_subset); eassumption.
- intros x Hx. rewrite in_union_iff in Hx.
destruct Hx; eapply (constants_of_term_form_subset); eassumption.
Qed.
Program Definition lower_term
{A K : Class} {n : nat}
(t : Term (S := zf_structure_over K) n) :
constants_of_term t ⊆ A →
Term (S := zf_structure_over A) n :=
match t with
| const _ c ⇒ fun H ⇒ const _ (element c)
| var x ⇒ fun H ⇒ var x
end.
Next Obligation. apply H. rewrite in_singleton_iff. reflexivity. Qed.
Program Fixpoint lower_formula
{A K : Class} {n : nat} (ϕ : Formula_Over K n) :
constants_of ϕ ⊆ A →
Formula_Over A n :=
match ϕ with
| exist ϕ ⇒ fun H ⇒ exist (lower_formula ϕ _)
| and ϕ ψ ⇒ fun H ⇒ and (lower_formula ϕ _) (lower_formula ψ _)
| not ϕ ⇒ fun H ⇒ not (lower_formula ϕ _)
| equal t1 t2 ⇒ fun H ⇒ equal (lower_term t1 _) (lower_term t2 _)
| is_element t1 t2 ⇒ fun H ⇒ is_element (lower_term t1 _) (lower_term t2 _)
end.
Next Obligation. apply H. rewrite in_union_iff. left. assumption. Qed.
Next Obligation. apply H. rewrite in_union_iff. right. assumption. Qed.
Next Obligation. apply H. rewrite in_union_iff. left. assumption. Qed.
Next Obligation. apply H. rewrite in_union_iff. right. assumption. Qed.
Next Obligation. apply H. rewrite in_union_iff. left. assumption. Qed.
Next Obligation. apply H. rewrite in_union_iff. right. assumption. Qed.
Definition lift_env {A K : Class} {n} (env : Vector.t A n) `{A ⊆ K} :
Vector.t K n :=
Vector.map (fun x : A ⇒ element x) env.
Fixpoint eval_over
{S : ZF_Structure} (A : Class)
{n: nat} (ϕ : Formula n) (env : Vector.t S n)
: Prop :=
match ϕ with
| exist ϕ ⇒ ∃ x : A, eval_over A ϕ ((x : S) :: env)
| and ϕ ψ ⇒ eval_over A ϕ env ∧ eval_over A ψ env
| not ϕ ⇒ ¬ eval_over A ϕ env
| equal t1 t2 ⇒ eval_term t1 env = eval_term t2 env
| is_element t1 t2 ⇒ eval_term t1 env ∈ eval_term t2 env
end.
Check Vector.In.
Fixpoint Vector_In {A} (x : A) {n} : Vector.t A n → Prop :=
match n with
| 0 ⇒ fun _ ⇒ False
| n.+1 ⇒ fun v ⇒ x = Vector.hd v ∨ Vector_In x (Vector.tl v)
end.
Definition Reflects
(A K : Class) {A_sub_K : A ⊆ K}
{n} (ϕ : Formula n) :=
∀ env : Vector.t A n,
(eval_over A ϕ (Vector.map element_value env) ↔
eval_over K ϕ (Vector.map element_value env)).
Program Definition ordinal_max (α β : ordinals) : ordinals :=
@ordinal_limit _ `{α, β} _.
Next Obligation.
rewrite in_unordered_pair_iff in H. destruct H as [-> | ->]; exact _.
Qed.
Instance left_sub_ordinal_max (α β : ordinals) :
α ⊆ ordinal_max α β.
Admitted.
Instance right_sub_ordinal_max (α β : ordinals) :
β ⊆ ordinal_max α β.
Admitted.
Lemma subset_of_L_is_subset_of_a_stage (A : S) :
A ⊆ L_as_class →
∃ α, A ⊆ L_stage α.
Admitted.
Lemma L_is_cumulative (α β : ordinals) :
α ⊆ β →
L_stage α ⊆ L_stage β.
Admitted.
Instance stage_sub_L (α : ordinals) :
L_stage α ⊆ L_as_class.
Proof.
intros x Hx. ∃ α. exact Hx.
Qed.
Lemma eval_term_on_lower_term
{A K : Class} (H1 : A ⊆ K)
{n} (t : Term (S := zf_structure_over K) n)
(H2 : constants_of_term t ⊆ A)
(env : Vector.t A n) :
(eval_term (lower_term t H2) env : S) = eval_term t (lift_env env).
Proof.
destruct t; cbn.
- reflexivity.
- symmetry.
pose (VectorSpec.nth_map (fun x : A ⇒ element x) env t t eq_refl).
apply element_equality in e.
exact e.
Qed.
Definition least (P : ordinals → Prop) {H : ∃ α, P α} : ordinals.
Admitted.
Lemma least_is_solution P {H} :
P (least P (H := H)).
Admitted.
Global Instance union_of_ordinals_is_ordinal (α β : S) :
α ∈ ordinals →
β ∈ ordinals →
α ∪ β ∈ ordinals.
Admitted.
Global Instance indexed_union_of_ordinals_is_ordinal
(I : Set_Like) (F : I → S) `{Is_Definable F} :
(∀ i, F i ∈ ordinals) →
(⋃ i : I, F i) ∈ ordinals.
Admitted.
Lemma L_stage_of_union (α β : S) `{α ∈ ordinals} `{β ∈ ordinals} :
L_stage (element (α ∪ β)) = L_stage (element α) ∪ L_stage (element β).
Admitted.
Global Instance L_stage_is_definable :
Is_Definable L_stage.
Admitted.
Lemma L_stage_of_indexed_union
(I : Set_Like) (F : I → S) `{Is_Definable F} `{∀ i, F i ∈ ordinals} :
L_stage (element (⋃ i : I, F i)) = ⋃ i : I, L_stage (element (F i)).
Admitted.
Lemma in_stage_of_indexed_union
(I : Set_Like) (F : I → S) `{Is_Definable F} `{∀ i, F i ∈ ordinals}
(x : S) :
x ∈ (⋃ i : I, L_stage (element (F i))) →
x ∈ L_stage (element (⋃ i : I, F i)).
Admitted.
Lemma L_stage_is_monotone (α β : ordinals) :
α ⊆ β →
L_stage α ⊆ L_stage β.
Admitted.
Lemma strip_element (A : Class) (x : A) (H : x ∈ A) :
build_element x H = x.
Admitted.
Global Instance Encoding_Of_Vector n A :
Encoding_Of A →
Encoding_Of (Vector.t A n).
Admitted.
Global Instance Encoding_Of_Vector_Is_A_Set n A (enc : Encoding_Of A) :
Is_A_Set enc →
Is_A_Set (Encoding_Of_Vector n A enc).
Admitted.
Global Instance encoding_of_nat :
Encoding_Of nat.
Admitted.
Global Instance encoding_of_nat_is_a_set :
Is_A_Set encoding_of_nat.
Admitted.
Definition elements_of_vector {A : Class} {n} (v : Vector.t A n) : S.
Admitted.
Definition lower_vector {A : Class} {n} (v : Vector.t A n) (B : Class) :
elements_of_vector v ⊆ B →
Vector.t B n.
Admitted.
Lemma map_element_value_of_lower_vector
{A : Class} {n} (v : Vector.t A n) (B : Class)
(H : elements_of_vector v ⊆ B) :
Vector.map element_value (lower_vector v B H) =
Vector.map element_value v.
Admitted.
Lemma elements_of_vector_in_countable_union
(F : nat → S) `{Is_Definable F}
{A : Class} {k} (v : Vector.t A k) :
(∀ n, F n ⊆ F n.+1) →
(A ⊆ ⋃ n : nat, F n) →
{ n & elements_of_vector v ⊆ F n }.
Admitted.
Lemma reflection_theorem
{n} (ϕ : Formula n) :
∀ α : ordinals,
{
β : ordinals |
α ⊆ β ∧
Reflects (L_stage β) L_as_class ϕ
}.
Proof.
induction ϕ.
- unshelve eset (f (α : ordinals) :=
least (fun β : ordinals ⇒
α ⊆ β ∧
Reflects (L_stage β) L_as_class ϕ)). {
destruct (IHϕ α) as [β Hβ]. ∃ β. exact Hβ.
}
unshelve eset (g (α : ordinals) :=
least (fun β : ordinals ⇒
α ⊆ β ∧
(∀ env : Vector.t (L_stage α) n,
(∃ x : L_as_class,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env)) →
(∃ x : L_stage β,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env))))). {
cbn.
unshelve eexists (element (
α ∪
⋃ env : Vector.t (L_stage α) n,
least (fun β ⇒
(∃ x : L_as_class,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env)) →
(∃ x : L_stage β,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env))))
).
- exact _.
- exact _.
- cbn.
destruct (classic (∃ x : L_as_class,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env))).
+ destruct H as [[x x_in_L] H].
unfold L_as_class in x_in_L. destruct x_in_L as [β x_in_stage].
∃ β. intros _. ∃ (element x). exact H.
+ ∃ ordinal_zero. intros ?. exfalso. apply H. exact H0.
- admit.
- apply union_of_ordinals_is_ordinal.
+ exact _.
+ simple refine (indexed_union_of_ordinals_is_ordinal _ _ _). admit.
- cbn. split.
+ intros x ?. apply in_union_iff. left. assumption.
+ intros env [x Hx].
eenough (∃ x' :
L_stage
(least (fun β ⇒
(∃ x : L_as_class,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env)) →
(∃ x : L_stage β,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env)))),
eval_over L_as_class ϕ ((x' : S) :: Vector.map element_value env)). {
destruct H as [x' Hx'].
unshelve eexists (element x'). {
rewrite L_stage_of_union. apply in_union_iff. right.
apply in_stage_of_indexed_union.
apply in_indexed_union_iff. cbn. ∃ env.
rewrite strip_element. exact _.
}
exact Hx'.
}
apply (least_is_solution (fun β ⇒ _ → ∃ x' : L_stage β, _)).
∃ x. exact Hx.
}
set (h α := nat_rect _ α (fun _ ⇒ f ∘ g)).
intros α.
unshelve eset (β := element (⋃ i : nat, h α i) : ordinals).
+ exact _.
+ exact _.
+ admit.
+ exact _.
+ ∃ β.
split.
× intros x ?. apply in_indexed_union_iff. cbn. ∃ 0. assumption.
× intros env. cbn.
assert (H1 : Reflects (L_stage β) L_as_class ϕ). admit.
split.
-- intros [y Hy]. ∃ (element y). rewrite <- (H1 (y :: env)). exact Hy.
-- intros [y Hy].
assert (k : { k : nat & elements_of_vector env ⊆ L_stage (h α k)}). {
unshelve eapply elements_of_vector_in_countable_union.
- admit.
- cbn. intros k.
assert (g (h α k) ⊆ f (g (h α k))). {
epose (least_is_solution (fun β ⇒ g (h α k) ⊆ β ∧ Reflects (L_stage β) L_as_class ϕ)) as H2.
cbn in H2. destruct H2 as [H2 _].
exact H2.
}
assert (h α k ⊆ g (h α k)). {
epose (least_is_solution
(fun β : ordinals ⇒
h α k ⊆ β ∧
(∀ env : Vector.t (L_stage (h α k)) n,
(∃ x : L_as_class,
eval_over L_as_class ϕ
((x : S) :: Vector.map element_value env)) →
∃ x : L_stage β,
eval_over L_as_class ϕ ((x : S) :: Vector.map element_value env)))) as H2.
destruct H2 as [H2 _]. exact H2.
}
apply L_stage_is_monotone.
intros x ?. apply H. apply H0. assumption.
- unfold β. rewrite L_stage_of_indexed_union. cbn.
intros x Hx. rewrite in_indexed_union_iff in Hx.
destruct Hx as [i Hx]. rewrite strip_element in Hx.
rewrite in_indexed_union_iff. ∃ i. exact Hx.
}
destruct k as [k Hk].
assert (H : h α k ⊆ g (h α k) ∧
∀ env : Vector.t (L_stage (h α k)) n,
(∃ x : L_as_class ,
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env)) →
(∃ x : L_stage (g (h α k)),
eval_over
L_as_class
ϕ
((x : S) :: Vector.map element_value env))). {
apply least_is_solution.
}
assert (z : ∃ z : L_stage (g (h α k)),
eval_over L_as_class ϕ ((z : S) :: Vector.map element_value env)). {
destruct H as [_ H].
specialize (H (lower_vector env _ Hk)).
rewrite <- (map_element_value_of_lower_vector _ _ _).
apply H. ∃ y. rewrite map_element_value_of_lower_vector. exact Hy.
}
destruct z as [z Hz].
assert (H2 : L_stage (g (h α k)) ⊆ L_stage β). {
admit.
}
∃ (element z).
specialize (H1 (element z :: env)).
apply H1.
exact Hz.
Admitted.
Lemma definable_subset_is_in_L (A : S) :
A ⊆ L_as_class →
(∃ ϕ : Formula_Over L_as_class 1, ∀ x : L_as_class, eval ϕ [x] ↔ x ∈ A) →
A ∈ L_as_class.
Admitted.
Lemma definable_subset_is_a_set_in_L
(P : L → Prop) :
Is_Definable_Over L_as_class P →
Is_A_Set (build_class (fun x : S ⇒ ∃ H : x ∈ L_as_class, P (element x))) →
Is_A_Set (build_class (S := L) P).
Proof.
intros definability [A HA].
assert (A ∈ L_as_class). {
apply definable_subset_is_in_L.
- intros x x_in_A. specialize (HA x). destruct HA as [_ HA].
specialize (HA x_in_A). destruct HA as [x_in_L _]. exact x_in_L.
- setoid_rewrite <- HA.
unfold element_relation; cbn.
admit.
}
∃ (element A).
intros x. specialize (HA x). rewrite <- HA.
split.
- intros Hx. ∃ _. replace (element (x : S)) with x.
+ exact Hx.
+ apply element_equality. reflexivity.
- intros [x_in_L P_x]. replace x with (element (x : S)).
+ exact P_x.
+ apply element_equality. reflexivity.
Admitted.
Program Definition empty_set_in_L : L :=
class_as_set (build_class (fun _ : L ⇒ False))
(is_a_set := _).
Next Obligation.
apply definable_subset_is_a_set_in_L.
- exact _.
- ∃ ∅.
split.
+ cbn. intros [_ []].
+ intros H. apply not_in_empty_set in H. contradiction.
Qed.
Program Definition unordered_pair_in_L (x y : L) : L :=
class_as_set (build_class (fun z : L ⇒ z = x ∨ z = y))
(is_a_set := _).
Next Obligation.
apply definable_subset_is_a_set_in_L.
- exact _.
- ∃ (`{element_value x, y}).
setoid_rewrite in_unordered_pair_iff. cbn. intros z.
unfold element_relation at 1. cbn.
setoid_rewrite <- element_equality. cbn.
split.
+ intros [_ H]. exact H.
+ intros [-> | ->]; ∃ _; auto.
Qed.
Program Definition power_set_in_L (A : L) : L :=
class_as_set (build_class (fun B : L ⇒ ∀ x : L, x ∈ B → x ∈ A))
(is_a_set := _).
Next Obligation.
change (L : Type) in A.
apply definable_subset_is_a_set_in_L.
- intros.
apply lambda_is_definable; intros.
simple notypeclasses refine (@forall_statement_is_definable L _ _ _ _ _ _ _).
+ exact _.
+ exact _.
+ change (Element_Of L_as_class) with (L : Type).
apply lambda_is_definable; intros.
refine (impl_is_definable (fun env : type'0 ⇒ x0 env ∈ x (r0 env))
(fun env ⇒ x0 env ∈ A)
_ _).
prove_that_application_is_definable. {
exact _.
}
prove_that_application_is_definable. {
exact _.
}
exact (weakening_on_type_with_encoding _ x r0 _).
- unshelve eexists (`{B ⊆ (A : S) | B ∈ L_as_class}).
intros B.
rewrite in_separation_iff. unfold element_relation at 1. cbn.
split.
+ intros [H1 H2]. split.
× rewrite in_power_set_iff.
intros x x_in_B.
unshelve eapply (H2 (element x)).
++ apply (L_is_transitive B); assumption.
++ assumption.
× assumption.
+ intros [B_sub_A B_in_L].
∃ B_in_L.
rewrite in_power_set_iff in B_sub_A.
intros x. apply B_sub_A.
Qed.
Program Definition big_union_in_L (A : L) : L :=
class_as_set (build_class (fun x : L ⇒ ∃ B : A, x ∈ B))
(is_a_set := _).
Next Obligation.
Admitted.
Program Definition infinite_set_in_L : L.
Admitted.
Program Definition relation_replacement_in_L
(R : L → L → Prop)
(definability : Is_Definable_Over L_as_class R)
(functionality : Is_Functional R)
(A : L)
: L :=
class_as_set (build_class (fun y ⇒ ∃ x : A, R x y))
(is_a_set := _).
Next Obligation.
apply definable_subset_is_a_set_in_L.
- intros.
apply lambda_is_definable; intros.
apply ex_statement_is_definable. {
exact _.
}
apply lambda_is_definable; intros.
prove_that_application_is_definable. {
exact _.
}
exact (weakening_on_type_with_encoding _ x r0 _).
- unshelve eexists (
relation_replacement
(fun x y : S ⇒ ∃ Hx : x ∈ L_as_class, ∃ Hy : y ∈ L_as_class,
R (element x) (element y))
_
_
A).
+ exact _.
+ exact _.
+ intros.
apply lambda_is_definable; intros.
apply lambda_is_definable; intros.
admit.
+ intros x y y' (Hx & Hy & H) (Hx' & Hy' & H').
enough (e : element y = element y'). {
apply element_equality in e. exact e.
}
apply (functionality (element x)).
× replace (build_element x Hx') with (build_element x Hx). {
exact H.
}
apply element_equality. reflexivity.
× exact H'.
+ intros y. rewrite in_relation_replacement_iff.
× cbn. split.
-- intros (y_in_L & x & H).
unshelve eexists (element ((x : L) : S)). {
exact (element_property _ x).
}
cbn. ∃ _. ∃ _.
replace (element ((x : L) : S)) with (x : L). {
exact H.
}
apply element_equality. reflexivity.
-- intros (x & Hx & Hy & H). ∃ _.
unshelve eexists (element (element x : L)).
++ exact Hx.
++ exact (element_property _ x).
++ cbn. exact H.
Admitted.
Definition zf_operations_on_L : ZF_Operations L :=
{|
empty_set := empty_set_in_L;
unordered_pair := unordered_pair_in_L;
power_set := power_set_in_L;
big_union := big_union_in_L;
infinite_set := infinite_set_in_L;
relation_replacement := relation_replacement_in_L
|}.
Program Definition constructible_model : ZF_Model :=
{| zf_operations := zf_operations_on_L |}.
Next Obligation.
apply element_equality. apply extensionality.
split.
- intros Hx.
unshelve eapply (H (element x)). {
apply (L_is_transitive A).
- exact _.
- assumption.
}
assumption.
- intros Hx.
unshelve eapply (H (element x)). {
apply (L_is_transitive B).
- exact _.
- assumption.
}
assumption.
Qed.
Next Obligation.
intros P step x.
enough (∀ x, ∀ H : x ∈ L_as_class, P (element x)). {
specialize (H x _).
replace (element ((x : L) : S)) with (x : L) in H.
- exact H.
- apply element_equality. reflexivity.
}
clear x.
refine (foundation _ _).
intros x IH x_in_L.
apply step. intros [y y_in_L] y_in_x. cbn in ×.
revert y_in_L.
apply (IH y y_in_x).
Qed.
Next Obligation.
intros H. apply in_class_as_set_iff in H.
contradiction.
Qed.
Next Obligation.
unfold unordered_pair_in_L. rewrite in_class_as_set_iff. reflexivity.
Qed.
Next Obligation.
unfold power_set_in_L. rewrite in_class_as_set_iff. reflexivity.
Qed.
Next Obligation.
unfold big_union_in_L. rewrite in_class_as_set_iff. reflexivity.
Qed.
Next Obligation.
admit.
Admitted.
Next Obligation.
unfold relation_replacement_in_L. rewrite in_class_as_set_iff. reflexivity.
Qed.
End L.