# Theory CM

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 (*>*)