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