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>‹forcing_data1›› 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›› locale G_generic1_AC = G_generic1 + M_ctm1_AC end