Theory Proper_Extension
section‹Separative notions and proper extensions›
theory Proper_Extension
imports
Names
begin
text‹The key ingredient to obtain a proper extension is to have
a ∗‹separative preorder›:›
locale separative_notion = forcing_notion +
assumes separative: "p∈ℙ ⟹ ∃q∈ℙ. ∃r∈ℙ. q ≼ p ∧ r ≼ p ∧ q ⊥ r"
begin
text‹For separative preorders, the complement of every filter is
dense. Hence an $M$-generic filter cannot belong to the ground model.›
lemma filter_complement_dense:
assumes "filter(G)"
shows "dense(ℙ - G)"
proof
fix p
assume "p∈ℙ"
show "∃d∈ℙ - G. d ≼ p"
proof (cases "p∈G")
case True
note ‹p∈ℙ› assms
moreover
obtain q r where "q ≼ p" "r ≼ p" "q ⊥ r" "q∈ℙ" "r∈ℙ"
using separative[OF ‹p∈ℙ›]
by force
with ‹filter(G)›
obtain s where "s ≼ p" "s ∉ G" "s ∈ ℙ"
using filter_imp_compat[of G q r]
by auto
then
show ?thesis
by blast
next
case False
with ‹p∈ℙ›
show ?thesis
using refl_leq unfolding Diff_def by auto
qed
qed
end
locale ctm_separative = forcing_data1 + separative_notion
begin
context
fixes G
assumes generic: "M_generic(G)"
begin
interpretation G_generic1 ℙ leq 𝟭 M enum G
by unfold_locales (simp add:generic)
lemma generic_not_in_M:
shows "G ∉ M"
proof
assume "G∈M"
then
have "ℙ - G ∈ M"
using Diff_closed by simp
moreover
have "¬(∃q∈G. q ∈ ℙ - G)" "(ℙ - G) ⊆ ℙ"
unfolding Diff_def by auto
moreover
note generic
ultimately
show "False"
using filter_complement_dense[of G] M_generic_denseD[of "ℙ-G"]
by auto
qed
theorem proper_extension: "M ≠ M[G]"
using generic G_in_Gen_Ext one_in_G generic_not_in_M
by force
end
end
end