subsection‹Application to Cohen posets\label{sec:cohen}› theory Cohen_Posets imports Delta_System begin text‹We end this session by applying DSL to the combinatorics of finite function posets. We first define some basic concepts; we take a different approach from \<^cite>‹"2020arXiv200109715G"›, in that the order relation is presented as a predicate (of type @{typ ‹[i,i] ⇒ o›}). Two elements of a poset are ∗‹compatible› if they have a common lower bound.› definition compat_in :: "[i,[i,i]⇒o,i,i]⇒o" where "compat_in(A,r,p,q) ≡ ∃d∈A . r(d,p) ∧ r(d,q)" text‹An ∗‹antichain› is a subset of pairwise incompatible members.› definition antichain :: "[i,[i,i]⇒o,i]⇒o" where "antichain(P,leq,A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A. p≠q ⟶ ¬compat_in(P,leq,p,q))" text‹A poset has the ∗‹countable chain condition› (ccc) if all of its antichains are countable.› definition ccc :: "[i,[i,i]⇒o]⇒o" where "ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ countable(A)" text‹Finally, the ∗‹Cohen poset› is the set of finite partial functions between two sets with the order of reverse inclusion.› definition Fn :: "[i,i] ⇒ i" where "Fn(I,J) ≡ ⋃{(d→J) . d ∈ {x ∈ Pow(I). Finite(x)}}" abbreviation Supset :: "i ⇒ i ⇒ o" (infixl ‹⊇› 50) where "f ⊇ g ≡ g ⊆ f" lemma FnI[intro]: assumes "p : d → J" "d ⊆ I" "Finite(d)" shows "p ∈ Fn(I,J)" using assms unfolding Fn_def by auto lemma FnD[dest]: assumes "p ∈ Fn(I,J)" shows "∃d. p : d → J ∧ d ⊆ I ∧ Finite(d)" using assms unfolding Fn_def by auto lemma Fn_is_function: "p ∈ Fn(I,J) ⟹ function(p)" unfolding Fn_def using fun_is_function by auto lemma restrict_eq_imp_compat: assumes "f ∈ Fn(I, J)" "g ∈ Fn(I, J)" "restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))" shows "f ∪ g ∈ Fn(I, J)" proof - from assms obtain d1 d2 where "f : d1 → J" "d1 ∈ Pow(I)" "Finite(d1)" "g : d2 → J" "d2 ∈ Pow(I)" "Finite(d2)" by blast with assms show ?thesis using domain_of_fun restrict_eq_imp_Un_into_Pi[of f d1 "λ_. J" g d2 "λ_. J"] by auto qed text‹We finally arrive to our application of DSL.› lemma ccc_Fn_2: "ccc(Fn(I,2), (⊇))" proof - { fix A assume "¬ countable(A)" assume "A ⊆ Fn(I, 2)" moreover from this have "countable({p∈A. domain(p) = d})" for d proof (cases "Finite(d) ∧ d ⊆ I") case True with ‹A ⊆ Fn(I, 2)› have "{p ∈ A . domain(p) = d} ⊆ d → 2" using domain_of_fun by fastforce moreover from True have "Finite(d → 2)" using Finite_Pi lesspoll_nat_is_Finite by auto ultimately show ?thesis using subset_Finite[of _ "d→2" ] Finite_imp_countable by auto next case False with ‹A ⊆ Fn(I, 2)› have "{p ∈ A . domain(p) = d} = 0" by (intro equalityI) (auto dest!: domain_of_fun) then show ?thesis using empty_lepollI by auto qed moreover have "uncountable({domain(p) . p ∈ A})" proof from ‹A ⊆ Fn(I, 2)› have "A = (⋃d∈{domain(p) . p ∈ A}. {p∈A. domain(p) = d})" by auto moreover assume "countable({domain(p) . p ∈ A})" moreover note ‹⋀d. countable({p∈A. domain(p) = d})› ‹¬countable(A)› ultimately show "False" using countable_imp_countable_UN[of "{domain(p). p∈A}" "λd. {p ∈ A. domain(p) = d }"] by auto qed moreover from ‹A ⊆ Fn(I, 2)› have "p ∈ A ⟹ Finite(domain(p))" for p using lesspoll_nat_is_Finite[of "domain(p)"] domain_of_fun[of p _ "λ_. 2"] by auto ultimately obtain D where "delta_system(D)" "D ⊆ {domain(p) . p ∈ A}" "D ≈ ℵ⇘1⇙" using delta_system_uncountable[of "{domain(p) . p ∈ A}"] by auto then have delta:"∀d1∈D. ∀d2∈D. d1 ≠ d2 ⟶ d1 ∩ d2 = ⋂D" using delta_system_root_eq_Inter by simp moreover from ‹D ≈ ℵ⇘1⇙› have "uncountable(D)" using uncountable_iff_subset_eqpoll_Aleph1 by auto moreover from this and ‹D ⊆ {domain(p) . p ∈ A}› obtain p1 where "p1 ∈ A" "domain(p1) ∈ D" using uncountable_not_empty[of D] by blast moreover from this and ‹p1 ∈ A ⟹ Finite(domain(p1))› have "Finite(domain(p1))" using Finite_domain by simp moreover define r where "r ≡ ⋂D" ultimately have "Finite(r)" using subset_Finite[of "r" "domain(p1)"] by auto have "countable({restrict(p,r) . p∈A})" proof - have "f ∈ Fn(I, 2) ⟹ restrict(f,r) ∈ Pow(r × 2)" for f using restrict_subset_Sigma[of f _ "λ_. 2" r] by (force simp: Pi_def) with ‹A ⊆ Fn(I, 2)› have "{restrict(f,r) . f ∈ A } ⊆ Pow(r × 2)" by fast with ‹Finite(r)› show ?thesis using Finite_Sigma[THEN Finite_Pow, of r "λ_. 2"] by (intro Finite_imp_countable) (auto intro:subset_Finite) qed moreover have "uncountable({p∈A. domain(p) ∈ D})" (is "uncountable(?X)") proof from ‹D ⊆ {domain(p) . p ∈ A}› have "(λp∈?X. domain(p)) ∈ surj(?X, D)" using lam_type unfolding surj_def by auto moreover assume "countable(?X)" moreover note ‹uncountable(D)› ultimately show False using surj_countable by auto qed moreover have "D = (⋃f∈Pow(r×2) . {domain(p) . p∈{ x∈A. restrict(x,r) = f ∧ domain(x) ∈ D}})" proof - { fix z assume "z ∈ D" with ‹D ⊆ _› obtain p where "domain(p) = z" "p ∈ A" by auto moreover from ‹A ⊆ Fn(I, 2)› and this have "p : z → 2" using domain_of_fun by force moreover from this have "restrict(p,r) ⊆ r × 2" using function_restrictI[of p r] fun_is_function[of p z "λ_. 2"] restrict_subset_Sigma[of p z "λ_. 2" r] by (auto simp:Pi_def) ultimately have "∃p∈A. restrict(p,r) ∈ Pow(r×2) ∧ domain(p) = z" by auto } then show ?thesis by (intro equalityI) (force)+ qed obtain f where "uncountable({domain(p) . p∈{x∈A. restrict(x,r) = f ∧ domain(x) ∈ D}})" (is "uncountable(?Y(f))") proof - { from ‹Finite(r)› have "countable(Pow(r×2))" using Finite_Sigma[THEN Finite_Pow, THEN Finite_imp_countable] by simp moreover assume "countable(?Y(f))" for f moreover note ‹D = (⋃f∈Pow(r×2) .?Y(f))› moreover note ‹uncountable(D)› ultimately have "False" using countable_imp_countable_UN[of "Pow(r×2)" ?Y] by auto } with that show ?thesis by auto qed then obtain j where "j ∈ inj(nat, ?Y(f))" using uncountable_iff_nat_lt_cardinal[THEN iffD1, THEN leI, THEN cardinal_le_imp_lepoll, THEN lepollD] by auto then have "j`0 ≠ j`1" "j`0 ∈ ?Y(f)" "j`1 ∈ ?Y(f)" using inj_is_fun[THEN apply_type, of j nat "?Y(f)"] unfolding inj_def by auto then obtain p q where "domain(p) ≠ domain(q)" "p ∈ A" "q ∈ A" "domain(p) ∈ D" "domain(q) ∈ D" "restrict(p,r) = restrict(q,r)" by auto moreover from this and delta have "domain(p) ∩ domain(q) = r" unfolding r_def by simp moreover note ‹A ⊆ Fn(I, 2)› moreover from calculation have "p ∪ q ∈ Fn(I, 2)" by (rule_tac restrict_eq_imp_compat) auto ultimately have "∃p∈A. ∃q∈A. p ≠ q ∧ compat_in(Fn(I, 2), (⊇), p, q)" unfolding compat_in_def by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast } then show ?thesis unfolding ccc_def antichain_def by auto qed text‹The fact that a poset $P$ has the ccc has useful consequences for the theory of forcing, since it implies that cardinals from the original model are exactly the cardinals in any generic extension by $P$ \<^cite>‹‹Chap.~IV› in "kunen2011set"›.› end