section‹Forcing notions›
text‹This theory defines a locale for forcing notions, that is,
preorders with a distinguished maximum element.›
theory Forcing_Notions
imports ZF "ZF-Constructible-Trans.Relative"
begin
subsection‹Basic concepts›
text‹We say that two elements $p,q$ are
∗‹compatible› if they have a lower bound in $P$›
definition compat_in :: "i⇒i⇒i⇒i⇒o" where
"compat_in(A,r,p,q) == ∃d∈A . ⟨d,p⟩∈r ∧ ⟨d,q⟩∈r"
definition
is_compat_in :: "[i⇒o,i,i,i,i] ⇒ o" where
"is_compat_in(M,A,r,p,q) ≡ ∃d[M]. d∈A ∧ (∃dp[M]. pair(M,d,p,dp) ∧ dp∈r ∧
(∃dq[M]. pair(M,d,q,dq) ∧ dq∈r))"
lemma compat_inI :
"⟦ d∈A ; ⟨d,p⟩∈r ; ⟨d,g⟩∈r ⟧ ⟹ compat_in(A,r,p,g)"
by (auto simp add: compat_in_def)
lemma refl_compat:
"⟦ refl(A,r) ; ⟨p,q⟩ ∈ r | p=q | ⟨q,p⟩ ∈ r ; p∈A ; q∈A⟧ ⟹ compat_in(A,r,p,q)"
by (auto simp add: refl_def compat_inI)
lemma chain_compat:
"refl(A,r) ⟹ linear(A,r) ⟹ (∀p∈A.∀q∈A. compat_in(A,r,p,q))"
by (simp add: refl_compat linear_def)
lemma subset_fun_image: "f:N→P ⟹ f``N⊆P"
by (auto simp add: image_fun apply_funtype)
lemma refl_monot_domain: "refl(B,r) ⟹ A⊆B ⟹ refl(A,r)"
unfolding refl_def by blast
definition
antichain :: "i⇒i⇒i⇒o" where
"antichain(P,leq,A) == A⊆P ∧ (∀p∈A.∀q∈A.(¬ compat_in(P,leq,p,q)))"
definition
ccc :: "i ⇒ i ⇒ o" where
"ccc(P,leq) == ∀A. antichain(P,leq,A) ⟶ |A| ≤ nat"
locale forcing_notion =
fixes P leq one
assumes one_in_P: "one ∈ P"
and leq_preord: "preorder_on(P,leq)"
and one_max: "∀p∈P. <p,one>∈leq"
begin
abbreviation Leq :: "[i, i] ⇒ o" (infixl "≼" 50)
where "x ≼ y ≡ <x,y>∈leq"
lemma refl_leq:
"r∈P ⟹ r≼r"
using leq_preord unfolding preorder_on_def refl_def by simp
text‹A set $D$ is ∗‹dense› if every element $p\in P$ has a lower
bound in $D$.›
definition
dense :: "i⇒o" where
"dense(D) == ∀p∈P. ∃d∈D . d≼p"
text‹There is also a weaker definition which asks for
a lower bound in $D$ only for the elements below some fixed
element $q$.›
definition
dense_below :: "i⇒i⇒o" where
"dense_below(D,q) == ∀p∈P. p≼q ⟶ (∃d∈D. d∈P ∧ d≼p)"
lemma P_dense: "dense(P)"
by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)
definition
increasing :: "i⇒o" where
"increasing(F) == ∀x∈F. ∀ p ∈ P . x≼p ⟶ p∈F"
definition
compat :: "i⇒i⇒o" where
"compat(p,q) == compat_in(P,leq,p,q)"
lemma leq_transD: "a≼b ⟹ b≼c ⟹ a ∈ P⟹ b ∈ P⟹ c ∈ P⟹ a≼c"
using leq_preord trans_onD unfolding preorder_on_def by blast
lemma leq_reflI: "p∈P ⟹ p≼p"
using leq_preord unfolding preorder_on_def refl_def by blast
lemma compatD[dest!]: "compat(p,q) ⟹ ∃d∈P. d≼p ∧ d≼q"
unfolding compat_def compat_in_def .
abbreviation Incompatible :: "[i, i] ⇒ o" (infixl "⊥" 50)
where "p ⊥ q ≡ ¬ compat(p,q)"
lemma compatI[intro!]: "d∈P ⟹ d≼p ⟹ d≼q ⟹ compat(p,q)"
unfolding compat_def compat_in_def by blast
lemma denseD [dest]: "dense(D) ⟹ p∈P ⟹ ∃d∈D. d≼ p"
unfolding dense_def by blast
lemma denseI [intro!]: "⟦ ⋀p. p∈P ⟹ ∃d∈D. d≼ p ⟧ ⟹ dense(D)"
unfolding dense_def by blast
lemma dense_belowD [dest]:
assumes "dense_below(D,p)" "q∈P" "q≼p"
shows "∃d∈D. d∈P ∧ d≼q"
using assms unfolding dense_below_def by simp
lemma dense_belowI [intro!]:
assumes "⋀q. q∈P ⟹ q≼p ⟹ ∃d∈D. d∈P ∧ d≼q"
shows "dense_below(D,p)"
using assms unfolding dense_below_def by simp
lemma dense_below_cong: "p∈P ⟹ D = D' ⟹ dense_below(D,p) ⟷ dense_below(D',p)"
by blast
lemma dense_below_cong': "p∈P ⟹ ⟦⋀x. x∈P ⟹ Q(x) ⟷ Q'(x)⟧ ⟹
dense_below({q∈P. Q(q)},p) ⟷ dense_below({q∈P. Q'(q)},p)"
by blast
lemma dense_below_mono: "p∈P ⟹ D ⊆ D' ⟹ dense_below(D,p) ⟹ dense_below(D',p)"
by blast
lemma dense_below_under:
assumes "dense_below(D,p)" "p∈P" "q∈P" "q≼p"
shows "dense_below(D,q)"
using assms leq_transD by blast
lemma ideal_dense_below:
assumes "⋀q. q∈P ⟹ q≼p ⟹ q∈D"
shows "dense_below(D,p)"
using assms leq_reflI by blast
lemma dense_below_dense_below:
assumes "dense_below({q∈P. dense_below(D,q)},p)" "p∈P"
shows "dense_below(D,p)"
using assms leq_transD leq_reflI by blast
definition
antichain :: "i⇒o" where
"antichain(A) == A⊆P ∧ (∀p∈A.∀q∈A.(¬compat(p,q)))"
text‹A filter is an increasing set $G$ with all its elements
being compatible in $G$.›
definition
filter :: "i⇒o" where
"filter(G) == G⊆P ∧ increasing(G) ∧ (∀p∈G. ∀q∈G. compat_in(G,leq,p,q))"
lemma filterD : "filter(G) ⟹ x ∈ G ⟹ x ∈ P"
by (auto simp add : subsetD filter_def)
lemma filter_leqD : "filter(G) ⟹ x ∈ G ⟹ y ∈ P ⟹ x≼y ⟹ y ∈ G"
by (simp add: filter_def increasing_def)
lemma filter_imp_compat: "filter(G) ⟹ p∈G ⟹ q∈G ⟹ compat(p,q)"
unfolding filter_def compat_in_def compat_def by blast
lemma low_bound_filter:
assumes "filter(G)" and "p∈G" and "q∈G"
shows "∃r∈G. r≼p ∧ r≼q"
using assms
unfolding compat_in_def filter_def by blast
text‹We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.›
definition
upclosure :: "i⇒i" where
"upclosure(A) == {p∈P.∃a∈A. a≼p}"
lemma upclosureI [intro] : "p∈P ⟹ a∈A ⟹ a≼p ⟹ p∈upclosure(A)"
by (simp add:upclosure_def, auto)
lemma upclosureE [elim] :
"p∈upclosure(A) ⟹ (⋀x a. x∈P ⟹ a∈A ⟹ a≼x ⟹ R) ⟹ R"
by (auto simp add:upclosure_def)
lemma upclosureD [dest] :
"p∈upclosure(A) ⟹ ∃a∈A.(a≼p) ∧ p∈P"
by (simp add:upclosure_def)
lemma upclosure_increasing :
"A⊆P ⟹ increasing(upclosure(A))"
apply (unfold increasing_def upclosure_def, simp)
apply clarify
apply (rule_tac x="a" in bexI)
apply (insert leq_preord, unfold preorder_on_def)
apply (drule conjunct2, unfold trans_on_def)
apply (drule_tac x="a" in bspec, fast)
apply (drule_tac x="x" in bspec, assumption)
apply (drule_tac x="p" in bspec, assumption)
apply (simp, assumption)
done
lemma upclosure_in_P: "A ⊆ P ⟹ upclosure(A) ⊆ P"
apply (rule subsetI)
apply (simp add:upclosure_def)
done
lemma A_sub_upclosure: "A ⊆ P ⟹ A⊆upclosure(A)"
apply (rule subsetI)
apply (simp add:upclosure_def, auto)
apply (insert leq_preord, unfold preorder_on_def refl_def, auto)
done
lemma elem_upclosure: "A⊆P ⟹ x∈A ⟹ x∈upclosure(A)"
by (blast dest:A_sub_upclosure)
lemma closure_compat_filter:
"A⊆P ⟹ (∀p∈A.∀q∈A. compat_in(A,leq,p,q)) ⟹ filter(upclosure(A))"
apply (unfold filter_def)
apply (intro conjI)
apply (rule upclosure_in_P, assumption)
apply (rule upclosure_increasing, assumption)
apply (unfold compat_in_def)
apply (rule ballI)+
apply (rename_tac x y)
apply (drule upclosureD)+
apply (erule bexE)+
apply (rename_tac a b)
apply (drule_tac A="A"
and x="a" in bspec, assumption)
apply (drule_tac A="A"
and x="b" in bspec, assumption)
apply (auto)
apply (rule_tac x="d" in bexI)
prefer 2 apply (simp add:A_sub_upclosure [THEN subsetD])
apply (insert leq_preord, unfold preorder_on_def trans_on_def, drule conjunct2)
apply (rule conjI)
apply (drule_tac x="d" in bspec, rule_tac A="A" in subsetD, assumption+)
apply (drule_tac x="a" in bspec, rule_tac A="A" in subsetD, assumption+)
apply (drule_tac x="x" in bspec, assumption, auto)
done
lemma aux_RS1: "f ∈ N → P ⟹ n∈N ⟹ f`n ∈ upclosure(f ``N)"
apply (rule_tac elem_upclosure)
apply (rule subset_fun_image, assumption)
apply (simp add: image_fun, blast)
done
lemma decr_succ_decr: "f ∈ nat → P ⟹ preorder_on(P,leq) ⟹
∀n∈nat. ⟨f ` succ(n), f ` n⟩ ∈ leq ⟹
n∈nat ⟹ m∈nat ⟹ n≤m ⟶ ⟨f ` m, f ` n⟩ ∈ leq"
apply (unfold preorder_on_def, erule conjE)
apply (induct_tac m, simp add:refl_def, rename_tac x)
apply (rule impI)
apply (case_tac "n≤x", simp)
apply (drule_tac x="x" in bspec, assumption)
apply (unfold trans_on_def)
apply (drule_tac x="f`succ(x)" in bspec, simp)
apply (drule_tac x="f`x" in bspec, simp)
apply (drule_tac x="f`n" in bspec, auto)
apply (drule_tac le_succ_iff [THEN iffD1], simp add: refl_def)
done
lemma decr_seq_linear: "refl(P,leq) ⟹ f ∈ nat → P ⟹
∀n∈nat. ⟨f ` succ(n), f ` n⟩ ∈ leq ⟹
trans[P](leq) ⟹ linear(f `` nat, leq)"
apply (unfold linear_def)
apply (rule ball_image_simp [THEN iffD2], assumption, simp, rule ballI)+
apply (rename_tac y)
apply (case_tac "x≤y")
apply (drule_tac n="x" and m="y" in decr_succ_decr)
apply (simp add:preorder_on_def)
apply (simp+)
apply (drule not_le_iff_lt[THEN iffD1, THEN leI, rotated 2], simp_all)
apply (drule_tac n="y" and m="x" in decr_succ_decr)
apply (simp add:preorder_on_def)
apply (simp+)
done
end
subsection‹Towards Rasiowa-Sikorski Lemma (RSL)›
locale countable_generic = forcing_notion +
fixes 𝒟
assumes countable_subs_of_P: "𝒟 ∈ nat→Pow(P)"
and seq_of_denses: "∀n ∈ nat. dense(𝒟`n)"
begin
definition
D_generic :: "i⇒o" where
"D_generic(G) == filter(G) ∧ (∀n∈nat.(𝒟`n)∩G≠0)"
text‹The next lemma identifies a sufficient condition for obtaining
RSL.›
lemma RS_sequence_imp_rasiowa_sikorski:
assumes
"p∈P" "f : nat→P" "f ` 0 = p"
"⋀n. n∈nat ⟹ f ` succ(n)≼ f ` n ∧ f ` succ(n) ∈ 𝒟 ` n"
shows
"∃G. p∈G ∧ D_generic(G)"
proof -
note assms
moreover from this
have "f``nat ⊆ P"
by (simp add:subset_fun_image)
moreover from calculation
have "refl(f``nat, leq) ∧ trans[P](leq)"
using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
moreover from calculation
have "∀n∈nat. f ` succ(n)≼ f ` n" by (simp)
moreover from calculation
have "linear(f``nat, leq)"
using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
moreover from calculation
have "(∀p∈f``nat.∀q∈f``nat. compat_in(f``nat,leq,p,q))"
using chain_compat by (auto)
ultimately
have "filter(upclosure(f``nat))" (is "filter(?G)")
using closure_compat_filter by simp
moreover
have "∀n∈nat. 𝒟 ` n ∩ ?G ≠ 0"
proof
fix n
assume "n∈nat"
with assms
have "f`succ(n) ∈ ?G ∧ f`succ(n) ∈ 𝒟 ` n"
using aux_RS1 by simp
then
show "𝒟 ` n ∩ ?G ≠ 0" by blast
qed
moreover from assms
have "p ∈ ?G"
using aux_RS1 by auto
ultimately
show ?thesis unfolding D_generic_def by auto
qed
end
text‹Now, the following recursive definition will fulfill the
requirements of lemma \<^term>‹RS_sequence_imp_rasiowa_sikorski› ›
consts RS_seq :: "[i,i,i,i,i,i] ⇒ i"
primrec
"RS_seq(0,P,leq,p,enum,𝒟) = p"
"RS_seq(succ(n),P,leq,p,enum,𝒟) =
enum`(μ m. ⟨enum`m, RS_seq(n,P,leq,p,enum,𝒟)⟩ ∈ leq ∧ enum`m ∈ 𝒟 ` n)"
context countable_generic
begin
lemma preimage_rangeD:
assumes "f∈Pi(A,B)" "b ∈ range(f)"
shows "∃a∈A. f`a = b"
using assms apply_equality[OF _ assms(1), of _ b] domain_type[OF _ assms(1)] by auto
lemma countable_RS_sequence_aux:
fixes p enum
defines "f(n) ≡ RS_seq(n,P,leq,p,enum,𝒟)"
and "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
"⋀x k. x∈P ⟹ k∈nat ⟹ ∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k"
shows
"f(succ(n)) ∈ P ∧ f(succ(n))≼ f(n) ∧ f(succ(n)) ∈ 𝒟 ` n"
using ‹n∈nat›
proof (induct)
case 0
from assms
obtain q where "q∈P" "q≼ p" "q ∈ 𝒟 ` 0" by blast
moreover from this and ‹P ⊆ range(enum)›
obtain m where "m∈nat" "enum`m = q"
using preimage_rangeD[OF ‹enum:nat→M›] by blast
moreover
have "𝒟`0 ⊆ P"
using apply_funtype[OF countable_subs_of_P] by simp
moreover note ‹p∈P›
ultimately
show ?case
using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
case (succ n)
with assms
obtain q where "q∈P" "q≼ f(succ(n))" "q ∈ 𝒟 ` succ(n)" by blast
moreover from this and ‹P ⊆ range(enum)›
obtain m where "m∈nat" "enum`m≼ f(succ(n))" "enum`m ∈ 𝒟 ` succ(n)"
using preimage_rangeD[OF ‹enum:nat→M›] by blast
moreover note succ
moreover from calculation
have "𝒟`succ(n) ⊆ P"
using apply_funtype[OF countable_subs_of_P] by auto
ultimately
show ?case
using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed
lemma countable_RS_sequence:
fixes p enum
defines "f ≡ λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)"
and "Q(q,k,m) ≡ enum`m≼ q ∧ enum`m ∈ 𝒟 ` k"
assumes "n∈nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
shows
"f`0 = p" "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n) ∈ P"
proof -
from assms
show "f`0 = p" by simp
{
fix x k
assume "x∈P" "k∈nat"
then
have "∃q∈P. q≼ x ∧ q ∈ 𝒟 ` k"
using seq_of_denses apply_funtype[OF countable_subs_of_P]
unfolding dense_def by blast
}
with assms
show "f`succ(n)≼ f`n ∧ f`succ(n) ∈ 𝒟 ` n" "f`succ(n)∈P"
unfolding f_def using countable_RS_sequence_aux by simp_all
qed
lemma RS_seq_type:
assumes "n ∈ nat" "p∈P" "P ⊆ range(enum)" "enum:nat→M"
shows "RS_seq(n,P,leq,p,enum,𝒟) ∈ P"
using assms countable_RS_sequence(1,3)
by (induct;simp)
lemma RS_seq_funtype:
assumes "p∈P" "P ⊆ range(enum)" "enum:nat→M"
shows "(λn∈nat. RS_seq(n,P,leq,p,enum,𝒟)): nat → P"
using assms lam_type RS_seq_type by auto
lemmas countable_rasiowa_sikorski =
RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]
end
end