section ‹ Closed Mereology › (*<*) theory CM imports M begin (*>*) text ‹ The theory of \emph{closed mereology} adds to ground mereology conditions guaranteeing the existence of sums and products.\footnote{See \<^cite>‹"masolo_atomicity_1999"› p. 238. \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"› p. 43 give a slightly weaker version of the sum closure axiom, which is equivalent given axioms considered later.} › locale CM = M + assumes sum_eq: "x ⊕ y = (THE z. ∀v. O v z ⟷ O v x ∨ O v y)" assumes sum_closure: "∃z. ∀v. O v z ⟷ O v x ∨ O v y" assumes product_eq: "x ⊗ y = (THE z. ∀v. P v z ⟷ P v x ∧ P v y)" assumes product_closure: "O x y ⟹ ∃z. ∀v. P v z ⟷ P v x ∧ P v y" begin subsection ‹ Products › lemma product_intro: "(∀w. P w z ⟷ (P w x ∧ P w y)) ⟹ x ⊗ y = z" proof - assume z: "∀w. P w z ⟷ (P w x ∧ P w y)" hence "(THE v. ∀w. P w v ⟷ P w x ∧ P w y) = z" proof (rule the_equality) fix v assume v: "∀w. P w v ⟷ (P w x ∧ P w y)" have "∀w. P w v ⟷ P w z" proof fix w from z have "P w z ⟷ (P w x ∧ P w y)".. moreover from v have "P w v ⟷ (P w x ∧ P w y)".. ultimately show "P w v ⟷ P w z" by (rule ssubst) qed with part_extensionality show "v = z".. qed thus "x ⊗ y = z" using product_eq by (rule subst) qed lemma product_idempotence: "x ⊗ x = x" proof - have "∀w. P w x ⟷ P w x ∧ P w x" proof fix w show "P w x ⟷ P w x ∧ P w x" proof assume "P w x" thus "P w x ∧ P w x" using ‹P w x›.. next assume "P w x ∧ P w x" thus "P w x".. qed qed thus "x ⊗ x = x" by (rule product_intro) qed lemma product_character: "O x y ⟹ (∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y))" proof - assume "O x y" hence "∃z. ∀w. P w z ⟷ (P w x ∧ P w y)" by (rule product_closure) then obtain z where z: "∀w. P w z ⟷ (P w x ∧ P w y)".. hence "x ⊗ y = z" by (rule product_intro) thus "∀w. P w (x ⊗ y) ⟷ P w x ∧ P w y" using z by (rule ssubst) qed lemma product_commutativity: "O x y ⟹ x ⊗ y = y ⊗ x" proof - assume "O x y" hence "O y x" by (rule overlap_symmetry) hence "∀w. P w (y ⊗ x) ⟷ (P w y ∧ P w x)" by (rule product_character) hence "∀w. P w (y ⊗ x) ⟷ (P w x ∧ P w y)" by auto thus "x ⊗ y = y ⊗ x" by (rule product_intro) qed lemma product_in_factors: "O x y ⟹ P (x ⊗ y) x ∧ P (x ⊗ y) y" proof - assume "O x y" hence "∀w. P w (x ⊗ y) ⟷ P w x ∧ P w y" by (rule product_character) hence "P (x ⊗ y) (x ⊗ y) ⟷ P (x ⊗ y) x ∧ P (x ⊗ y) y".. moreover have "P (x ⊗ y) (x ⊗ y)" by (rule part_reflexivity) ultimately show "P (x ⊗ y) x ∧ P (x ⊗ y) y".. qed lemma product_in_first_factor: "O x y ⟹ P (x ⊗ y) x" proof - assume "O x y" hence "P (x ⊗ y) x ∧ P (x ⊗ y) y" by (rule product_in_factors) thus "P (x ⊗ y) x".. qed lemma product_in_second_factor: "O x y ⟹ P (x ⊗ y) y" proof - assume "O x y" hence "P (x ⊗ y) x ∧ P (x ⊗ y) y" by (rule product_in_factors) thus "P (x ⊗ y) y".. qed lemma nonpart_implies_proper_product: "¬ P x y ∧ O x y ⟹ PP (x ⊗ y) x" proof - assume antecedent: "¬ P x y ∧ O x y" hence "¬ P x y".. from antecedent have "O x y".. hence "P (x ⊗ y) x" by (rule product_in_first_factor) moreover have "(x ⊗ y) ≠ x" proof assume "(x ⊗ y) = x" hence "¬ P (x ⊗ y) y" using ‹¬ P x y› by (rule ssubst) moreover have "P (x ⊗ y) y" using ‹O x y› by (rule product_in_second_factor) ultimately show "False".. qed ultimately have "P (x ⊗ y) x ∧ x ⊗ y ≠ x".. with nip_eq show "PP (x ⊗ y) x".. qed lemma common_part_in_product: "P z x ∧ P z y ⟹ P z (x ⊗ y)" proof - assume antecedent: "P z x ∧ P z y" hence "∃z. P z x ∧ P z y".. with overlap_eq have "O x y".. hence "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)" by (rule product_character) hence "P z (x ⊗ y) ⟷ (P z x ∧ P z y)".. thus "P z (x ⊗ y)" using ‹P z x ∧ P z y›.. qed lemma product_part_in_factors: "O x y ⟹ P z (x ⊗ y) ⟹ P z x ∧ P z y" proof - assume "O x y" hence "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)" by (rule product_character) hence "P z (x ⊗ y) ⟷ (P z x ∧ P z y)".. moreover assume "P z (x ⊗ y)" ultimately show "P z x ∧ P z y".. qed corollary product_part_in_first_factor: "O x y ⟹ P z (x ⊗ y) ⟹ P z x" proof - assume "O x y" moreover assume "P z (x ⊗ y)" ultimately have "P z x ∧ P z y" by (rule product_part_in_factors) thus "P z x".. qed corollary product_part_in_second_factor: "O x y ⟹ P z (x ⊗ y) ⟹ P z y" proof - assume "O x y" moreover assume "P z (x ⊗ y)" ultimately have "P z x ∧ P z y" by (rule product_part_in_factors) thus "P z y".. qed lemma part_product_identity: "P x y ⟹ x ⊗ y = x" proof - assume "P x y" with part_reflexivity have "P x x ∧ P x y".. hence "P x (x ⊗ y)" by (rule common_part_in_product) have "O x y" using ‹P x y› by (rule part_implies_overlap) hence "P (x ⊗ y) x" by (rule product_in_first_factor) thus "x ⊗ y = x" using ‹P x (x ⊗ y)› by (rule part_antisymmetry) qed lemma product_overlap: "P z x ⟹ O z y ⟹ O z (x ⊗ y)" proof - assume "P z x" assume "O z y" with overlap_eq have "∃v. P v z ∧ P v y".. then obtain v where v: "P v z ∧ P v y".. hence "P v y".. from v have "P v z".. hence "P v x" using ‹P z x› by (rule part_transitivity) hence "P v x ∧ P v y" using ‹P v y›.. hence "P v (x ⊗ y)" by (rule common_part_in_product) with ‹P v z› have "P v z ∧ P v (x ⊗ y)".. hence "∃v. P v z ∧ P v (x ⊗ y)".. with overlap_eq show "O z (x ⊗ y)".. qed lemma disjoint_from_second_factor: "P x y ∧ ¬ O x (y ⊗ z) ⟹ ¬ O x z" proof - assume antecedent: "P x y ∧ ¬ O x (y ⊗ z)" hence "¬ O x (y ⊗ z)".. show "¬ O x z" proof from antecedent have "P x y".. moreover assume "O x z" ultimately have "O x (y ⊗ z)" by (rule product_overlap) with ‹¬ O x (y ⊗ z)› show "False".. qed qed lemma converse_product_overlap: "O x y ⟹ O z (x ⊗ y) ⟹ O z y" proof - assume "O x y" hence "P (x ⊗ y) y" by (rule product_in_second_factor) moreover assume "O z (x ⊗ y)" ultimately show "O z y" by (rule overlap_monotonicity) qed lemma part_product_in_whole_product: "O x y ⟹ P x v ∧ P y z ⟹ P (x ⊗ y) (v ⊗ z)" proof - assume "O x y" assume "P x v ∧ P y z" have "∀w. P w (x ⊗ y) ⟶ P w (v ⊗ z)" proof fix w show "P w (x ⊗ y) ⟶ P w (v ⊗ z)" proof assume "P w (x ⊗ y)" with ‹O x y› have "P w x ∧ P w y" by (rule product_part_in_factors) have "P w v ∧ P w z" proof from ‹P w x ∧ P w y› have "P w x".. moreover from ‹P x v ∧ P y z› have "P x v".. ultimately show "P w v" by (rule part_transitivity) next from ‹P w x ∧ P w y› have "P w y".. moreover from ‹P x v ∧ P y z› have "P y z".. ultimately show "P w z" by (rule part_transitivity) qed thus "P w (v ⊗ z)" by (rule common_part_in_product) qed qed hence "P (x ⊗ y) (x ⊗ y) ⟶ P (x ⊗ y) (v ⊗ z)".. moreover have "P (x ⊗ y) (x ⊗ y)" by (rule part_reflexivity) ultimately show "P (x ⊗ y) (v ⊗ z)".. qed lemma right_associated_product: "(∃w. P w x ∧ P w y ∧ P w z) ⟹ (∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z))" proof - assume antecedent: "(∃w. P w x ∧ P w y ∧ P w z)" then obtain w where w: "P w x ∧ P w y ∧ P w z".. hence "P w x".. from w have "P w y ∧ P w z".. hence "∃w. P w y ∧ P w z".. with overlap_eq have "O y z".. hence yz: "∀w. P w (y ⊗ z) ⟷ (P w y ∧ P w z)" by (rule product_character) hence "P w (y ⊗ z) ⟷ (P w y ∧ P w z)".. hence "P w (y ⊗ z)" using ‹P w y ∧ P w z›.. with ‹P w x› have "P w x ∧ P w (y ⊗ z)".. hence "∃w. P w x ∧ P w (y ⊗ z)".. with overlap_eq have "O x (y ⊗ z)".. hence xyz: "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ P w (y ⊗ z)" by (rule product_character) show "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z)" proof fix w from yz have wyz: "P w (y ⊗ z) ⟷ (P w y ∧ P w z)".. moreover from xyz have "P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ P w (y ⊗ z)".. ultimately show "P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z)" by (rule subst) qed qed lemma left_associated_product: "(∃w. P w x ∧ P w y ∧ P w z) ⟹ (∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z)" proof - assume antecedent: "(∃w. P w x ∧ P w y ∧ P w z)" then obtain w where w: "P w x ∧ P w y ∧ P w z".. hence "P w y ∧ P w z".. hence "P w y".. have "P w z" using ‹P w y ∧ P w z›.. from w have "P w x".. hence "P w x ∧ P w y" using ‹P w y›.. hence "∃z. P z x ∧ P z y".. with overlap_eq have "O x y".. hence xy: "∀w. P w (x ⊗ y) ⟷ (P w x ∧ P w y)" by (rule product_character) hence "P w (x ⊗ y) ⟷ (P w x ∧ P w y)".. hence "P w (x ⊗ y)" using ‹P w x ∧ P w y›.. hence "P w (x ⊗ y) ∧ P w z" using ‹P w z›.. hence "∃w. P w (x ⊗ y) ∧ P w z".. with overlap_eq have "O (x ⊗ y) z".. hence xyz: "∀w. P w ((x ⊗ y) ⊗ z) ⟷ P w (x ⊗ y) ∧ P w z" by (rule product_character) show "∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z" proof fix v from xy have vxy: "P v (x ⊗ y) ⟷ (P v x ∧ P v y)".. moreover from xyz have "P v ((x ⊗ y) ⊗ z) ⟷ P v (x ⊗ y) ∧ P v z".. ultimately show "P v ((x ⊗ y) ⊗ z) ⟷ (P v x ∧ P v y) ∧ P v z" by (rule subst) qed qed theorem product_associativity: "(∃w. P w x ∧ P w y ∧ P w z) ⟹ x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z" proof - assume ante:"(∃w. P w x ∧ P w y ∧ P w z)" hence "(∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w x ∧ (P w y ∧ P w z))" by (rule right_associated_product) moreover from ante have "(∀w. P w ((x ⊗ y) ⊗ z) ⟷ (P w x ∧ P w y) ∧ P w z)" by (rule left_associated_product) ultimately have "∀w. P w (x ⊗ (y ⊗ z)) ⟷ P w ((x ⊗ y) ⊗ z)" by simp with part_extensionality show "x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z".. qed end subsection ‹ Differences › text ‹ Some writers also add to closed mereology the axiom of difference closure.\footnote{See, for example, \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"masolo_atomicity_1999"› p. 238.} › locale CMD = CM + assumes difference_eq: "x ⊖ y = (THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" assumes difference_closure: "(∃w. P w x ∧ ¬ O w y) ⟹ (∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" begin lemma difference_intro: "(∀w. P w z ⟷ P w x ∧ ¬ O w y) ⟹ x ⊖ y = z" proof - assume antecedent: "(∀w. P w z ⟷ P w x ∧ ¬ O w y)" hence "(THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y) = z" proof (rule the_equality) fix v assume v: "(∀w. P w v ⟷ P w x ∧ ¬ O w y)" have "∀w. P w v ⟷ P w z" proof fix w from antecedent have "P w z ⟷ P w x ∧ ¬ O w y".. moreover from v have "P w v ⟷ P w x ∧ ¬ O w y".. ultimately show "P w v ⟷ P w z" by (rule ssubst) qed with part_extensionality show "v = z".. qed with difference_eq show "x ⊖ y = z" by (rule ssubst) qed lemma difference_idempotence: "¬ O x y ⟹ (x ⊖ y) = x" proof - assume "¬ O x y" hence "¬ O y x" by (rule disjoint_symmetry) have "∀w. P w x ⟷ P w x ∧ ¬ O w y" proof fix w show "P w x ⟷ P w x ∧ ¬ O w y" proof assume "P w x" hence "¬ O y w" using ‹¬ O y x› by (rule disjoint_demonotonicity) hence "¬ O w y" by (rule disjoint_symmetry) with ‹P w x› show "P w x ∧ ¬ O w y".. next assume "P w x ∧ ¬ O w y" thus "P w x".. qed qed thus "(x ⊖ y) = x" by (rule difference_intro) qed lemma difference_character: "(∃w. P w x ∧ ¬ O w y) ⟹ (∀w. P w (x ⊖ y) ⟷ P w x ∧ ¬ O w y)" proof - assume "∃w. P w x ∧ ¬ O w y" hence "∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y" by (rule difference_closure) then obtain z where z: "∀w. P w z ⟷ P w x ∧ ¬ O w y".. hence "(x ⊖ y) = z" by (rule difference_intro) thus "∀w. P w (x ⊖ y) ⟷ P w x ∧ ¬ O w y" using z by (rule ssubst) qed lemma difference_disjointness: "(∃z. P z x ∧ ¬ O z y) ⟹ ¬ O y (x ⊖ y)" proof - assume "∃z. P z x ∧ ¬ O z y" hence xmy: "∀w. P w (x ⊖ y) ⟷ (P w x ∧ ¬ O w y)" by (rule difference_character) show "¬ O y (x ⊖ y)" proof assume "O y (x ⊖ y)" with overlap_eq have "∃v. P v y ∧ P v (x ⊖ y)".. then obtain v where v: "P v y ∧ P v (x ⊖ y)".. from xmy have "P v (x ⊖ y) ⟷ (P v x ∧ ¬ O v y)".. moreover from v have "P v (x ⊖ y)".. ultimately have "P v x ∧ ¬ O v y".. hence "¬ O v y".. moreover from v have "P v y".. hence "O v y" by (rule part_implies_overlap) ultimately show "False".. qed qed end subsection ‹ The Universe › text ‹ Another closure condition sometimes considered is the existence of the universe.\footnote{ See, for example, \<^cite>‹"varzi_parts_1996"› p. 264 and \<^cite>‹"casati_parts_1999"› p. 45.} › locale CMU = CM + assumes universe_eq: "u = (THE z. ∀w. P w z)" assumes universe_closure: "∃y. ∀x. P x y" begin lemma universe_intro: "(∀w. P w z) ⟹ u = z" proof - assume z: "∀w. P w z" hence "(THE z. ∀w. P w z) = z" proof (rule the_equality) fix v assume v: "∀w. P w v" have "∀w. P w v ⟷ P w z" proof fix w show "P w v ⟷ P w z" proof assume "P w v" from z show "P w z".. next assume "P w z" from v show "P w v".. qed qed with part_extensionality show "v = z".. qed thus "u = z" using universe_eq by (rule subst) qed lemma universe_character: "P x u" proof - from universe_closure obtain y where y: "∀x. P x y".. hence "u = y" by (rule universe_intro) hence "∀x. P x u" using y by (rule ssubst) thus "P x u".. qed lemma "¬ PP u x" proof assume "PP u x" hence "¬ P x u" by (rule proper_implies_not_part) thus "False" using universe_character.. qed lemma product_universe_implies_factor_universe: "O x y ⟹ x ⊗ y = u ⟹ x = u" proof - assume "x ⊗ y = u" moreover assume "O x y" hence "P (x ⊗ y) x" by (rule product_in_first_factor) ultimately have "P u x" by (rule subst) with universe_character show "x = u" by (rule part_antisymmetry) qed end subsection ‹ Complements › text ‹ As is a condition ensuring the existence of complements.\footnote{See, for example, \<^cite>‹"varzi_parts_1996"› p. 264 and \<^cite>‹"casati_parts_1999"› p. 45.} › locale CMC = CM + assumes complement_eq: "─x = (THE z. ∀w. P w z ⟷ ¬ O w x)" assumes complement_closure: "(∃w. ¬ O w x) ⟹ (∃z. ∀w. P w z ⟷ ¬ O w x)" assumes difference_eq: "x ⊖ y = (THE z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" begin lemma complement_intro: "(∀w. P w z ⟷ ¬ O w x) ⟹ ─x = z" proof - assume antecedent: "∀w. P w z ⟷ ¬ O w x" hence "(THE z. ∀w. P w z ⟷ ¬ O w x) = z" proof (rule the_equality) fix v assume v: "∀w. P w v ⟷ ¬ O w x" have "∀w. P w v ⟷ P w z" proof fix w from antecedent have "P w z ⟷ ¬ O w x".. moreover from v have "P w v ⟷ ¬ O w x".. ultimately show "P w v ⟷ P w z" by (rule ssubst) qed with part_extensionality show "v = z".. qed with complement_eq show "─x = z" by (rule ssubst) qed lemma complement_character: "(∃w. ¬ O w x) ⟹ (∀w. P w (─x) ⟷ ¬ O w x)" proof - assume "∃w. ¬ O w x" hence "(∃z. ∀w. P w z ⟷ ¬ O w x)" by (rule complement_closure) then obtain z where z: "∀w. P w z ⟷ ¬ O w x".. hence "─x = z" by (rule complement_intro) thus "∀w. P w (─x) ⟷ ¬ O w x" using z by (rule ssubst) qed lemma not_complement_part: "∃w. ¬ O w x ⟹ ¬ P x (─x)" proof - assume "∃w. ¬ O w x" hence "∀w. P w (─x) ⟷ ¬ O w x" by (rule complement_character) hence "P x (─x) ⟷ ¬ O x x".. show "¬ P x (─x)" proof assume "P x (─x)" with ‹P x (─x) ⟷ ¬ O x x› have "¬ O x x".. thus "False" using overlap_reflexivity.. qed qed lemma complement_part: "¬ O x y ⟹ P x (─y)" proof - assume "¬ O x y" hence "∃z. ¬ O z y".. hence "∀w. P w (─y) ⟷ ¬ O w y" by (rule complement_character) hence "P x (─y) ⟷ ¬ O x y".. thus "P x (─y)" using ‹¬ O x y›.. qed lemma complement_overlap: "¬ O x y ⟹ O x (─y)" proof - assume "¬ O x y" hence "P x (─y)" by (rule complement_part) thus "O x (─y)" by (rule part_implies_overlap) qed lemma or_complement_overlap: "∀y. O y x ∨ O y (─x)" proof fix y show "O y x ∨ O y (─x)" proof cases assume "O y x" thus "O y x ∨ O y (─x)".. next assume "¬ O y x" hence "O y (─x)" by (rule complement_overlap) thus "O y x ∨ O y (─x)".. qed qed lemma complement_disjointness: "∃v. ¬ O v x ⟹ ¬ O x (─x)" proof - assume "∃v. ¬ O v x" hence w: "∀w. P w (─x) ⟷ ¬ O w x" by (rule complement_character) show "¬ O x (─x)" proof assume "O x (─x)" with overlap_eq have "∃v. P v x ∧ P v (─x)".. then obtain v where v: "P v x ∧ P v (─x)".. from w have "P v (─x) ⟷ ¬ O v x".. moreover from v have "P v (─x)".. ultimately have "¬ O v x".. moreover from v have "P v x".. hence "O v x" by (rule part_implies_overlap) ultimately show "False".. qed qed lemma part_disjoint_from_complement: "∃v. ¬ O v x ⟹ P y x ⟹ ¬ O y (─x)" proof assume "∃v. ¬ O v x" hence "¬ O x (─x)" by (rule complement_disjointness) assume "P y x" assume "O y (─x)" with overlap_eq have "∃v. P v y ∧ P v (─x)".. then obtain v where v: "P v y ∧ P v (─x)".. hence "P v y".. hence "P v x" using ‹P y x› by (rule part_transitivity) moreover from v have "P v (─x)".. ultimately have "P v x ∧ P v (─x)".. hence "∃v. P v x ∧ P v (─x)".. with overlap_eq have "O x (─x)".. with ‹¬ O x (─x)› show "False".. qed lemma product_complement_character: "(∃w. P w x ∧ ¬ O w y) ⟹ (∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ (¬ O w y)))" proof - assume antecedent: "∃w. P w x ∧ ¬ O w y" then obtain w where w: "P w x ∧ ¬ O w y".. hence "P w x".. moreover from w have "¬ O w y".. hence "P w (─y)" by (rule complement_part) ultimately have "P w x ∧ P w (─y)".. hence "∃w. P w x ∧ P w (─y)".. with overlap_eq have "O x (─y)".. hence prod: "(∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ P w (─y)))" by (rule product_character) show "∀w. P w (x ⊗ (─y)) ⟷ (P w x ∧ (¬ O w y))" proof fix v from w have "¬ O w y".. hence "∃w. ¬ O w y".. hence "∀w. P w (─y) ⟷ ¬ O w y" by (rule complement_character) hence "P v (─y) ⟷ ¬ O v y".. moreover have "P v (x ⊗ (─y)) ⟷ (P v x ∧ P v (─y))" using prod.. ultimately show "P v (x ⊗ (─y)) ⟷ (P v x ∧ (¬ O v y))" by (rule subst) qed qed theorem difference_closure: "(∃w. P w x ∧ ¬ O w y) ⟹ (∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" proof - assume "∃w. P w x ∧ ¬ O w y" hence "∀w. P w (x ⊗ (─y)) ⟷ P w x ∧ ¬ O w y" by (rule product_complement_character) thus "(∃z. ∀w. P w z ⟷ P w x ∧ ¬ O w y)" by (rule exI) qed end sublocale CMC ⊆ CMD proof fix x y show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" using difference_eq. show "(∃w. P w x ∧ ¬ O w y) ⟹ (∃z. ∀w. P w z = (P w x ∧ ¬ O w y))" using difference_closure. qed corollary (in CMC) difference_is_product_of_complement: "(∃w. P w x ∧ ¬ O w y) ⟹ (x ⊖ y) = x ⊗ (─y)" proof - assume antecedent: "∃w. P w x ∧ ¬ O w y" hence "∀w. P w (x ⊗ (─y)) ⟷ P w x ∧ ¬ O w y" by (rule product_complement_character) thus "(x ⊖ y) = x ⊗ (─y)" by (rule difference_intro) qed text ‹ Universe and difference closure entail complement closure, since the difference of an individual and the universe is the individual's complement. › locale CMUD = CMU + CMD + assumes complement_eq: "─x = (THE z. ∀w. P w z ⟷ ¬ O w x)" begin lemma universe_difference: "(∃w. ¬ O w x) ⟹ (∀w. P w (u ⊖ x) ⟷ ¬ O w x)" proof - assume "∃w. ¬ O w x" then obtain w where w: "¬ O w x".. from universe_character have "P w u". hence "P w u ∧ ¬ O w x" using ‹¬ O w x›.. hence "∃z. P z u ∧ ¬ O z x".. hence ux: "∀w. P w (u ⊖ x) ⟷ (P w u ∧ ¬ O w x)" by (rule difference_character) show "∀w. P w (u ⊖ x) ⟷ ¬ O w x" proof fix w from ux have wux: "P w (u ⊖ x) ⟷ (P w u ∧ ¬ O w x)".. show "P w (u ⊖ x) ⟷ ¬ O w x" proof assume "P w (u ⊖ x)" with wux have "P w u ∧ ¬ O w x".. thus "¬ O w x".. next assume "¬ O w x" from universe_character have "P w u". hence "P w u ∧ ¬ O w x" using ‹¬ O w x›.. with wux show "P w (u ⊖ x)".. qed qed qed theorem complement_closure: "(∃w. ¬ O w x) ⟹ (∃z. ∀w. P w z ⟷ ¬ O w x)" proof - assume "∃w. ¬ O w x" hence "∀w. P w (u ⊖ x) ⟷ ¬ O w x" by (rule universe_difference) thus "∃z. ∀w. P w z ⟷ ¬ O w x".. qed end sublocale CMUD ⊆ CMC proof fix x y show "─x = (THE z. ∀w. P w z ⟷ (¬ O w x))" using complement_eq. show "∃w. ¬ O w x ⟹ ∃z. ∀w. P w z ⟷ (¬ O w x)" using complement_closure. show "x ⊖ y = (THE z. ∀w. P w z = (P w x ∧ ¬ O w y))" using difference_eq. qed corollary (in CMUD) complement_universe_difference: "(∃y. ¬ O y x) ⟹ ─x = (u ⊖ x)" proof - assume "∃w. ¬ O w x" hence "∀w. P w (u ⊖ x) ⟷ ¬ O w x" by (rule universe_difference) thus " ─x = (u ⊖ x)" by (rule complement_intro) qed (*<*) end (*>*)