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∈P ⟹ ∃q∈P. ∃r∈P. q ≼ p ∧ r ≼ p ∧ q ⊥ r"
begin
text‹For separative preorders, the complement of every filter is
dense. Hence an $M$-generic filter can't belong to the ground model.›
lemma filter_complement_dense:
assumes "filter(G)" shows "dense(P - G)"
proof
fix p
assume "p∈P"
show "∃d∈P - G. d ≼ p"
proof (cases "p∈G")
case True
note ‹p∈P› assms
moreover
obtain q r where "q ≼ p" "r ≼ p" "q ⊥ r" "q∈P" "r∈P"
using separative[OF ‹p∈P›]
by force
with ‹filter(G)›
obtain s where "s ≼ p" "s ∉ G" "s ∈ P"
using filter_imp_compat[of G q r]
by auto
then
show ?thesis by blast
next
case False
with ‹p∈P›
show ?thesis using refl_leq unfolding Diff_def by auto
qed
qed
end
locale ctm_separative = forcing_data + separative_notion
begin
lemma generic_not_in_M: assumes "M_generic(G)" shows "G ∉ M"
proof
assume "G∈M"
then
have "P - G ∈ M"
using P_in_M Diff_closed by simp
moreover
have "¬(∃q∈G. q ∈ P - G)" "(P - G) ⊆ P"
unfolding Diff_def by auto
moreover
note assms
ultimately
show "False"
using filter_complement_dense[of G] M_generic_denseD[of G "P-G"]
M_generic_def by simp
qed
theorem proper_extension: assumes "M_generic(G)" shows "M ≠ M[G]"
using assms G_in_Gen_Ext[of G] one_in_G[of G] generic_not_in_M
by force
end
end