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