Theory Absolute_Versions
section‹From M to V›
theory Absolute_Versions
imports
Not_CH
ZF.Cardinal_AC
begin
subsection‹Locales of a class \<^term>‹M› hold in \<^term>‹𝒱››
interpretation V: M_trivial 𝒱
using Union_ax_absolute upair_ax_absolute
by unfold_locales auto
lemmas bad_simps= V.nonempty V.Forall_in_M_iff V.Inl_in_M_iff V.Inr_in_M_iff
V.succ_in_M_iff V.singleton_in_M_iff V.Equal_in_M_iff V.Member_in_M_iff V.Nand_in_M_iff
V.Cons_in_M_iff V.pair_in_M_iff V.upair_in_M_iff
lemmas bad_M_trivial_simps[simp del] = V.Forall_in_M_iff V.Equal_in_M_iff
V.nonempty
lemmas bad_M_trivial_rules[rule del] = V.pair_in_MI V.singleton_in_MI V.pair_in_MD V.nat_into_M
V.depth_closed V.length_closed V.nat_case_closed V.separation_closed
V.Un_closed V.strong_replacement_closed V.nonempty
interpretation V:M_basic 𝒱
using power_ax_absolute separation_absolute replacement_absolute
by unfold_locales auto
interpretation V:M_eclose 𝒱
by unfold_locales (auto intro:separation_absolute replacement_absolute
simp:iterates_replacement_def wfrec_replacement_def)
lemmas bad_M_basic_rules[simp del, rule del] =
V.cartprod_closed V.finite_funspace_closed V.converse_closed
V.list_case'_closed V.pred_closed
interpretation V:M_cardinal_arith 𝒱
by unfold_locales (auto intro:separation_absolute replacement_absolute
simp add:iterates_replacement_def wfrec_replacement_def lam_replacement_def)
lemmas bad_M_cardinals_rules[simp del, rule del] =
V.iterates_closed V.M_nat V.trancl_closed V.rvimage_closed
interpretation V:M_cardinal_arith_jump 𝒱
by unfold_locales (auto intro:separation_absolute replacement_absolute
simp:wfrec_replacement_def)
lemma choice_ax_Universe : "choice_ax(𝒱)"
proof -
{
fix x
obtain f where "f ∈ surj(|x|,x)"
using cardinal_eqpoll unfolding eqpoll_def bij_def by fast
moreover
have "Ord(|x|)" by simp
ultimately
have "∃a. Ord(a) ∧ (∃f. f ∈ surj(a,x))"
by fast
}
then
show ?thesis unfolding choice_ax_def rall_def rex_def
by simp
qed
interpretation V:M_master 𝒱
using choice_ax_Universe
by unfold_locales (auto intro:separation_absolute replacement_absolute
simp:lam_replacement_def transrec_replacement_def wfrec_replacement_def
is_wfrec_def M_is_recfun_def)
named_theorems V_simps
lemma eqpoll_rel_absolute [V_simps]: "x ≈⇗𝒱⇖ y ⟷ x ≈ y"
unfolding eqpoll_def using V.def_eqpoll_rel by auto
lemma cardinal_rel_absolute [V_simps]: "|x|⇗𝒱⇖ = |x|"
unfolding cardinal_def cardinal_rel_def by (simp add:V_simps)
lemma Card_rel_absolute [V_simps]:"Card⇗𝒱⇖(a) ⟷ Card(a)"
unfolding Card_rel_def Card_def by (simp add:V_simps)
lemma csucc_rel_absolute [V_simps]:"(a⇧+)⇗𝒱⇖ = a⇧+"
unfolding csucc_rel_def csucc_def by (simp add:V_simps)
lemma function_space_rel_absolute [V_simps]:"x →⇗𝒱⇖ y = x → y"
using V.function_space_rel_char by (simp add:V_simps)
lemma cexp_rel_absolute [V_simps]:"x⇗↑y,𝒱⇖ = x⇗↑y⇖"
unfolding cexp_rel_def cexp_def by (simp add:V_simps)
lemma HAleph_rel_absolute [V_simps]:"HAleph_rel(𝒱,a,b) = HAleph(a,b)"
unfolding HAleph_rel_def HAleph_def by (auto simp add:V_simps)
lemma Aleph_rel_absolute [V_simps]: "Ord(x) ⟹ ℵ⇘x⇙⇗𝒱⇖ = ℵ⇘x⇙"
proof -
assume "Ord(x)"
have "ℵ⇘x⇙⇗𝒱⇖ = transrec(x, λa b. HAleph_rel(𝒱,a,b))"
unfolding Aleph_rel_def by simp
also
have "… = transrec(x, HAleph)"
by (simp add:V_simps)
also from ‹Ord(x)›
have "… = ℵ⇘x⇙"
using Aleph'_eq_Aleph unfolding Aleph'_def by simp
finally
show ?thesis .
qed
txt‹Example of absolute lemmas obtained from the relative versions.
Note the ∗‹only› declarations›
lemma Ord_cardinal_idem' : "Ord(A) ⟹ ||A|| = |A|"
using V.Ord_cardinal_rel_idem by (simp only:V_simps)
lemma Aleph_succ' : "Ord(α) ⟹ ℵ⇘succ(α)⇙ = ℵ⇘α⇙⇧+"
using V.Aleph_rel_succ by (simp only:V_simps)
txt‹These two results are new, first obtained in relative form
(not ported).›
lemma csucc_cardinal :
assumes "Ord(κ)" shows "|κ|⇧+ = κ⇧+"
using assms V.csucc_rel_cardinal_rel by (simp add:V_simps)
lemma csucc_le_mono :
assumes "κ ≤ ν" shows "κ⇧+ ≤ ν⇧+"
using assms V.csucc_rel_le_mono by (simp add:V_simps)
txt‹Example of transferring results from a transitive model to \<^term>‹𝒱››
lemma (in M_Perm) eqpoll_rel_transfer_absolute :
assumes "M(A)" "M(B)" "A ≈⇗M⇖ B"
shows "A ≈ B"
proof -
interpret M_N_Perm M 𝒱
by (unfold_locales, simp only:V_simps)
from assms
show ?thesis using eqpoll_rel_transfer
by (simp only:V_simps)
qed
txt‹The “relationalized” $\CH$ with respect to \<^term>‹𝒱› corresponds
to the real $\CH$.›
lemma is_ContHyp_iff_CH : "is_ContHyp(𝒱) ⟷ ContHyp"
using V.is_ContHyp_iff
by (auto simp add:ContHyp_rel_def ContHyp_def V_simps)
end