section ‹ Extensional Mereology › (*<*) theory EM imports MM begin (*>*) text ‹ Extensional mereology adds to ground mereology the axiom of strong supplementation.\footnote{ See \<^cite>‹"simons_parts:_1987"› p. 29, \<^cite>‹"varzi_parts_1996"› p. 262 and \<^cite>‹"casati_parts_1999"› p. 39-40.} › locale EM = M + assumes strong_supplementation: "¬ P x y ⟹ (∃z. P z x ∧ ¬ O z y)" begin text ‹ Strong supplementation entails weak supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 29 and \<^cite>‹"casati_parts_1999"› p. 40.} › lemma weak_supplementation: "PP x y ⟹ (∃z. P z y ∧ ¬ O z x)" proof - assume "PP x y" hence "¬ P y x" by (rule proper_implies_not_part) thus "∃z. P z y ∧ ¬ O z x" by (rule strong_supplementation) qed end text ‹ So minimal mereology is a subtheory of extensional mereology.\footnote{\<^cite>‹"casati_parts_1999"› p. 40.} › sublocale EM ⊆ MM proof fix y x show "PP y x ⟹ ∃z. P z x ∧ ¬ O z y" using weak_supplementation. qed text ‹ Strong supplementation also entails the proper parts principle.\footnote{See \<^cite>‹"simons_parts:_1987"› pp. 28-9 and \<^cite>‹"varzi_parts_1996"› p. 263.} › context EM begin lemma proper_parts_principle: "(∃z. PP z x) ⟹ (∀z. PP z x ⟶ P z y) ⟹ P x y" proof - assume "∃z. PP z x" then obtain v where v: "PP v x".. hence "P v x" by (rule proper_implies_part) assume antecedent: "∀z. PP z x ⟶ P z y" hence "PP v x ⟶ P v y".. hence "P v y" using ‹PP v x›.. with ‹P v x› have "P v x ∧ P v y".. hence "∃v. P v x ∧ P v y".. with overlap_eq have "O x y".. show "P x y" proof (rule ccontr) assume "¬ P x y" hence "∃z. P z x ∧ ¬ O z y" by (rule strong_supplementation) then obtain z where z: "P z x ∧ ¬ O z y".. hence "P z x".. moreover have "z ≠ x" proof assume "z = x" moreover from z have "¬ O z y".. ultimately have "¬ O x y" by (rule subst) thus "False" using ‹O x y›.. qed ultimately have "P z x ∧ z ≠ x".. with nip_eq have "PP z x".. from antecedent have "PP z x ⟶ P z y".. hence "P z y" using ‹PP z x›.. hence "O z y" by (rule part_implies_overlap) from z have "¬ O z y".. thus "False" using ‹O z y›.. qed qed text ‹ Which with antisymmetry entails the extensionality of proper parthood.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 28, \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"› p. 40.} › theorem proper_part_extensionality: "(∃z. PP z x ∨ PP z y) ⟹ x = y ⟷ (∀z. PP z x ⟷ PP z y)" proof - assume antecedent: "∃z. PP z x ∨ PP z y" show "x = y ⟷ (∀z. PP z x ⟷ PP z y)" proof assume "x = y" moreover have "∀z. PP z x ⟷ PP z x" by simp ultimately show "∀z. PP z x ⟷ PP z y" by (rule subst) next assume right: "∀z. PP z x ⟷ PP z y" have "∀z. PP z x ⟶ P z y" proof fix z show "PP z x ⟶ P z y" proof assume "PP z x" from right have "PP z x ⟷ PP z y".. hence "PP z y" using ‹PP z x›.. thus "P z y" by (rule proper_implies_part) qed qed have "∀z. PP z y ⟶ P z x" proof fix z show "PP z y ⟶ P z x" proof assume "PP z y" from right have "PP z x ⟷ PP z y".. hence "PP z x" using ‹PP z y›.. thus "P z x" by (rule proper_implies_part) qed qed from antecedent obtain z where z: "PP z x ∨ PP z y".. thus "x = y" proof (rule disjE) assume "PP z x" hence "∃z. PP z x".. hence "P x y" using ‹∀z. PP z x ⟶ P z y› by (rule proper_parts_principle) from right have "PP z x ⟷ PP z y".. hence "PP z y" using ‹PP z x›.. hence "∃z. PP z y".. hence "P y x" using ‹∀z. PP z y ⟶ P z x› by (rule proper_parts_principle) with ‹P x y› show "x = y" by (rule part_antisymmetry) next assume "PP z y" hence "∃z. PP z y".. hence "P y x" using ‹∀z. PP z y ⟶ P z x› by (rule proper_parts_principle) from right have "PP z x ⟷ PP z y".. hence "PP z x" using ‹PP z y›.. hence "∃z. PP z x".. hence "P x y" using ‹∀z. PP z x ⟶ P z y› by (rule proper_parts_principle) thus "x = y" using ‹P y x› by (rule part_antisymmetry) qed qed qed text ‹ It also follows from strong supplementation that parthood is definable in terms of overlap.\footnote{ See \<^cite>‹"parsons_many_2014"› p. 4.} › lemma part_overlap_eq: "P x y ⟷ (∀z. O z x ⟶ O z y)" proof assume "P x y" show "(∀z. O z x ⟶ O z y)" proof fix z show "O z x ⟶ O z y" proof assume "O z x" with ‹P x y› show "O z y" by (rule overlap_monotonicity) qed qed next assume right: "∀z. O z x ⟶ O z y" show "P x y" proof (rule ccontr) assume "¬ P x y" hence "∃z. P z x ∧ ¬ O z y" by (rule strong_supplementation) then obtain z where z: "P z x ∧ ¬ O z y".. hence "¬ O z y".. from right have "O z x ⟶ O z y".. moreover from z have "P z x".. hence "O z x" by (rule part_implies_overlap) ultimately have "O z y".. with ‹¬ O z y› show "False".. qed qed text ‹ Which entails the extensionality of overlap. › theorem overlap_extensionality: "x = y ⟷ (∀z. O z x ⟷ O z y)" proof assume "x = y" moreover have "∀z. O z x ⟷ O z x" proof fix z show "O z x ⟷ O z x".. qed ultimately show "∀z. O z x ⟷ O z y" by (rule subst) next assume right: "∀z. O z x ⟷ O z y" have "∀z. O z y ⟶ O z x" proof fix z from right have "O z x ⟷ O z y".. thus "O z y ⟶ O z x".. qed with part_overlap_eq have "P y x".. have "∀z. O z x ⟶ O z y" proof fix z from right have "O z x ⟷ O z y".. thus "O z x ⟶ O z y".. qed with part_overlap_eq have "P x y".. thus "x = y" using ‹P y x› by (rule part_antisymmetry) qed end (*<*) end (*>*)