Theory Forcing_Data
section‹Transitive set models of ZF›
text‹This theory defines locales for countable transitive models of $\ZF$,
and on top of that, one that includes a forcing notion. Weakened versions
of both locales are included, that only assume finitely many replacement
instances.›
theory Forcing_Data
imports
Forcing_Notions
Cohen_Posets_Relative
ZF_Trans_Interpretations
begin
no_notation Aleph (‹ℵ_› [90] 90)
subsection‹A forcing locale and generic filters›
text‹Ideally, countability should be separated from the assumption of this locale.
The fact is that our present proofs of the “definition of forces” (and many
consequences) and of the lemma for “forcing a value” of function
unnecessarily depend on the countability of the ground model. ›
locale forcing_data1 = forcing_notion + M_ctm1 +
assumes P_in_M: "ℙ ∈ M"
and leq_in_M: "leq ∈ M"
locale forcing_data2 = forcing_data1 + M_ctm2_AC
locale forcing_data3 = forcing_data2 + M_ctm3_AC
context forcing_data1
begin
lemma P_sub_M : "ℙ ⊆ M"
using transitivity P_in_M by auto
definition
M_generic :: "i⇒o" where
"M_generic(G) ≡ filter(G) ∧ (∀D∈M. D⊆ℙ ∧ dense(D)⟶D∩G≠0)"
declare iff_trans [trans]
lemma M_generic_imp_filter[dest]: "M_generic(G) ⟹ filter(G)"
unfolding M_generic_def by blast
lemma generic_filter_existence:
"p∈ℙ ⟹ ∃G. p∈G ∧ M_generic(G)"
proof -
assume "p∈ℙ"
let ?D="λn∈nat. (if (enum`n⊆ℙ ∧ dense(enum`n)) then enum`n else ℙ)"
have "∀n∈nat. ?D`n ∈ Pow(ℙ)"
by auto
then
have "?D:nat→Pow(ℙ)"
using lam_type by auto
have "∀n∈nat. dense(?D`n)"
proof(intro ballI)
fix n
assume "n∈nat"
then
have "dense(?D`n) ⟷ dense(if enum`n ⊆ ℙ ∧ dense(enum`n) then enum`n else ℙ)"
by simp
also
have "... ⟷ (¬(enum`n ⊆ ℙ ∧ dense(enum`n)) ⟶ dense(ℙ)) "
using split_if by simp
finally
show "dense(?D`n)"
using P_dense ‹n∈nat› by auto
qed
with ‹?D∈_›
interpret cg: countable_generic ℙ leq 𝟭 ?D
by (unfold_locales, auto)
from ‹p∈ℙ›
obtain G where 1: "p∈G ∧ filter(G) ∧ (∀n∈nat.(?D`n)∩G≠0)"
using cg.countable_rasiowa_sikorski[where M="λ_. M"] P_sub_M
M_countable[THEN bij_is_fun] M_countable[THEN bij_is_surj, THEN surj_range]
unfolding cg.D_generic_def by blast
then
have "(∀D∈M. D⊆ℙ ∧ dense(D)⟶D∩G≠0)"
proof (intro ballI impI)
fix D
assume "D∈M" and 2: "D ⊆ ℙ ∧ dense(D) "
moreover
have "∀y∈M. ∃x∈nat. enum`x= y"
using M_countable and bij_is_surj unfolding surj_def by (simp)
moreover from calculation
obtain n where Eq10: "n∈nat ∧ enum`n = D"
by auto
moreover from calculation if_P
have "?D`n = D"
by simp
moreover
note 1
ultimately
show "D∩G≠0"
by auto
qed
with 1
show ?thesis
unfolding M_generic_def by auto
qed
lemma one_in_M: "𝟭 ∈ M"
using one_in_P P_in_M transitivity
by simp
declare P_in_M [simp,intro]
declare one_in_M [simp,intro]
declare leq_in_M [simp,intro]
declare one_in_P [intro]
end
locale G_generic1 = forcing_data1 +
fixes G :: "i"
assumes generic : "M_generic(G)"
begin
lemma G_nonempty: "G≠0"
using generic subset_refl[of ℙ] P_dense
unfolding M_generic_def
by auto
lemma M_genericD [dest]: "x∈G ⟹ x∈ℙ"
using generic
by (blast dest:filterD)
lemma M_generic_leqD [dest]: "p∈G ⟹ q∈ℙ ⟹ p≼q ⟹ q∈G"
using generic
by (blast dest:filter_leqD)
lemma M_generic_compatD [dest]: "p∈G ⟹ r∈G ⟹ ∃q∈G. q≼p ∧ q≼r"
using generic
by (blast dest:low_bound_filter)
lemma M_generic_denseD [dest]: "dense(D) ⟹ D⊆ℙ ⟹ D∈M ⟹ ∃q∈G. q∈D"
using generic
unfolding M_generic_def by blast
lemma G_subset_P: "G⊆ℙ"
using generic by auto
lemma one_in_G : "𝟭 ∈ G"
proof -
have "increasing(G)"
using generic
unfolding M_generic_def filter_def by simp
then
show ?thesis
using G_nonempty one_max
unfolding increasing_def by blast
qed
lemma G_subset_M: "G ⊆ M"
using generic transitivity[OF _ P_in_M] by auto
end
locale G_generic1_AC = G_generic1 + M_ctm1_AC
end