section ‹ Ground Mereology › (*<*) theory M imports PM begin (*>*) text ‹ The theory of \emph{ground mereology} adds to premereology the antisymmetry of parthood, and defines proper parthood as nonidentical parthood.\footnote{For this axiomatization of ground mereology see, for example, \<^cite>‹"varzi_parts_1996"› p. 261 and \<^cite>‹"casati_parts_1999"› p. 36. For discussion of the antisymmetry of parthood see, for example, \<^cite>‹"cotnoir_antisymmetry_2010"›. For the definition of proper parthood as nonidentical parthood, see for example, \<^cite>‹"leonard_calculus_1940"› p. 47.} In other words, ground mereology assumes that parthood is a partial order.› locale M = PM + assumes part_antisymmetry: "P x y ⟹ P y x ⟹ x = y" assumes nip_eq: "PP x y ⟷ P x y ∧ x ≠ y" begin subsection ‹ Proper Parthood › lemma proper_implies_part: "PP x y ⟹ P x y" proof - assume "PP x y" with nip_eq have "P x y ∧ x ≠ y".. thus "P x y".. qed lemma proper_implies_distinct: "PP x y ⟹ x ≠ y" proof - assume "PP x y" with nip_eq have "P x y ∧ x ≠ y".. thus "x ≠ y".. qed lemma proper_implies_not_part: "PP x y ⟹ ¬ P y x" proof - assume "PP x y" hence "P x y" by (rule proper_implies_part) show "¬ P y x" proof from ‹PP x y› have "x ≠ y" by (rule proper_implies_distinct) moreover assume "P y x" with ‹P x y› have "x = y" by (rule part_antisymmetry) ultimately show "False".. qed qed lemma proper_part_asymmetry: "PP x y ⟹ ¬ PP y x" proof - assume "PP x y" hence "P x y" by (rule proper_implies_part) from ‹PP x y› have "x ≠ y" by (rule proper_implies_distinct) show "¬ PP y x" proof assume "PP y x" hence "P y x" by (rule proper_implies_part) with ‹P x y› have "x = y" by (rule part_antisymmetry) with ‹x ≠ y› show "False".. qed qed lemma proper_implies_overlap: "PP x y ⟹ O x y" proof - assume "PP x y" hence "P x y" by (rule proper_implies_part) thus "O x y" by (rule part_implies_overlap) qed end text ‹ The rest of this section compares four alternative axiomatizations of ground mereology, and verifies their equivalence. › text ‹ The first alternative axiomatization defines proper parthood as nonmutual instead of nonidentical parthood.\footnote{ See, for example, \<^cite>‹"varzi_parts_1996"› p. 261 and \<^cite>‹"casati_parts_1999"› p. 36. For the distinction between nonmutual and nonidentical parthood, see \<^cite>‹"parsons_many_2014"› pp. 6-8.} In the presence of antisymmetry, the two definitions of proper parthood are equivalent.\footnote{ See \<^cite>‹"cotnoir_antisymmetry_2010"› p. 398, \<^cite>‹"donnelly_using_2011"› p. 233, \<^cite>‹"cotnoir_non-wellfounded_2012"› p. 191, \<^cite>‹"obojska_remarks_2013"› p. 344, \<^cite>‹"cotnoir_does_2016"› p. 128 and \<^cite>‹"cotnoir_is_2018"›.} › locale M1 = PM + assumes nmp_eq: "PP x y ⟷ P x y ∧ ¬ P y x" assumes part_antisymmetry: "P x y ⟹ P y x ⟹ x = y" sublocale M ⊆ M1 proof fix x y show nmp_eq: "PP x y ⟷ P x y ∧ ¬ P y x" proof assume "PP x y" with nip_eq have nip: "P x y ∧ x ≠ y".. hence "x ≠ y".. from nip have "P x y".. moreover have "¬ P y x" proof assume "P y x" with ‹P x y› have "x = y" by (rule part_antisymmetry) with ‹x ≠ y› show "False".. qed ultimately show "P x y ∧ ¬ P y x".. next assume nmp: "P x y ∧ ¬ P y x" hence "¬ P y x".. from nmp have "P x y".. moreover have "x ≠ y" proof assume "x = y" hence "¬ P y y" using ‹¬ P y x› by (rule subst) thus "False" using part_reflexivity.. qed ultimately have "P x y ∧ x ≠ y".. with nip_eq show "PP x y".. qed show "P x y ⟹ P y x ⟹ x = y" using part_antisymmetry. qed sublocale M1 ⊆ M proof fix x y show nip_eq: "PP x y ⟷ P x y ∧ x ≠ y" proof assume "PP x y" with nmp_eq have nmp: "P x y ∧ ¬ P y x".. hence "¬ P y x".. from nmp have "P x y".. moreover have "x ≠ y" proof assume "x = y" hence "¬ P y y" using ‹¬ P y x› by (rule subst) thus "False" using part_reflexivity.. qed ultimately show "P x y ∧ x ≠ y".. next assume nip: "P x y ∧ x ≠ y" hence "x ≠ y".. from nip have "P x y".. moreover have "¬ P y x" proof assume "P y x" with ‹P x y› have "x = y" by (rule part_antisymmetry) with ‹x ≠ y› show "False".. qed ultimately have "P x y ∧ ¬ P y x".. with nmp_eq show "PP x y".. qed show "P x y ⟹ P y x ⟹ x = y" using part_antisymmetry. qed text ‹ Conversely, assuming the two definitions of proper parthood are equivalent entails the antisymmetry of parthood, leading to the second alternative axiomatization, which assumes both equivalencies.\footnote{ For this point see especially \<^cite>‹"parsons_many_2014"› pp. 9-10.} › locale M2 = PM + assumes nip_eq: "PP x y ⟷ P x y ∧ x ≠ y" assumes nmp_eq: "PP x y ⟷ P x y ∧ ¬ P y x" sublocale M ⊆ M2 proof fix x y show "PP x y ⟷ P x y ∧ x ≠ y" using nip_eq. show "PP x y ⟷ P x y ∧ ¬ P y x" using nmp_eq. qed sublocale M2 ⊆ M proof fix x y show "PP x y ⟷ P x y ∧ x ≠ y" using nip_eq. show "P x y ⟹ P y x ⟹ x = y" proof - assume "P x y" assume "P y x" show "x = y" proof (rule ccontr) assume "x ≠ y" with ‹P x y› have "P x y ∧ x ≠ y".. with nip_eq have "PP x y".. with nmp_eq have "P x y ∧ ¬ P y x".. hence "¬ P y x".. thus "False" using ‹P y x›.. qed qed qed text ‹ In the context of the other axioms, antisymmetry is equivalent to the extensionality of parthood, which gives the third alternative axiomatization.\footnote{For this point see \<^cite>‹"cotnoir_antisymmetry_2010"› p. 401 and \<^cite>‹"cotnoir_non-wellfounded_2012"› p. 191-2.} › locale M3 = PM + assumes nip_eq: "PP x y ⟷ P x y ∧ x ≠ y" assumes part_extensionality: "x = y ⟷ (∀ z. P z x ⟷ P z y)" sublocale M ⊆ M3 proof fix x y show "PP x y ⟷ P x y ∧ x ≠ y" using nip_eq. show part_extensionality: "x = y ⟷ (∀ z. P z x ⟷ P z y)" proof assume "x = y" moreover have "∀ z. P z x ⟷ P z x" by simp ultimately show "∀ z. P z x ⟷ P z y" by (rule subst) next assume z: "∀ z. P z x ⟷ P z y" show "x = y" proof (rule part_antisymmetry) from z have "P y x ⟷ P y y".. moreover have "P y y" by (rule part_reflexivity) ultimately show "P y x".. next from z have "P x x ⟷ P x y".. moreover have "P x x" by (rule part_reflexivity) ultimately show "P x y".. qed qed qed sublocale M3 ⊆ M proof fix x y show "PP x y ⟷ P x y ∧ x ≠ y" using nip_eq. show part_antisymmetry: "P x y ⟹ P y x ⟹ x = y" proof - assume "P x y" assume "P y x" have "∀ z. P z x ⟷ P z y" proof fix z show "P z x ⟷ P z y" proof assume "P z x" thus "P z y" using ‹P x y› by (rule part_transitivity) next assume "P z y" thus "P z x" using ‹P y x› by (rule part_transitivity) qed qed with part_extensionality show "x = y".. qed qed text ‹The fourth axiomatization adopts proper parthood as primitive.\footnote{See, for example, \<^cite>‹"simons_parts:_1987"›, p. 26 and \<^cite>‹"casati_parts_1999"› p. 37.} Improper parthood is defined as proper parthood or identity.› locale M4 = assumes part_eq: "P x y ⟷ PP x y ∨ x = y" assumes overlap_eq: "O x y ⟷ (∃ z. P z x ∧ P z y)" assumes proper_part_asymmetry: "PP x y ⟹ ¬ PP y x" assumes proper_part_transitivity: "PP x y ⟹ PP y z ⟹ PP x z" begin lemma proper_part_irreflexivity: "¬ PP x x" proof assume "PP x x" hence "¬ PP x x" by (rule proper_part_asymmetry) thus "False" using ‹PP x x›.. qed end sublocale M ⊆ M4 proof fix x y z show part_eq: "P x y ⟷ (PP x y ∨ x = y)" proof assume "P x y" show "PP x y ∨ x = y" proof cases assume "x = y" thus "PP x y ∨ x = y".. next assume "x ≠ y" with ‹P x y› have "P x y ∧ x ≠ y".. with nip_eq have "PP x y".. thus "PP x y ∨ x = y".. qed next assume "PP x y ∨ x = y" thus "P x y" proof assume "PP x y" thus "P x y" by (rule proper_implies_part) next assume "x = y" thus "P x y" by (rule identity_implies_part) qed qed show "O x y ⟷ (∃ z. P z x ∧ P z y)" using overlap_eq. show "PP x y ⟹ ¬ PP y x" using proper_part_asymmetry. show proper_part_transitivity: "PP x y ⟹ PP y z ⟹ PP x z" proof - assume "PP x y" assume "PP y z" have "P x z ∧ x ≠ z" proof from ‹PP x y› have "P x y" by (rule proper_implies_part) moreover from ‹PP y z› have "P y z" by (rule proper_implies_part) ultimately show "P x z" by (rule part_transitivity) next show "x ≠ z" proof assume "x = z" hence "PP y x" using ‹PP y z› by (rule ssubst) hence "¬ PP x y" by (rule proper_part_asymmetry) thus "False" using ‹PP x y›.. qed qed with nip_eq show "PP x z".. qed qed sublocale M4 ⊆ M proof fix x y z show proper_part_eq: "PP x y ⟷ P x y ∧ x ≠ y" proof assume "PP x y" hence "PP x y ∨ x = y".. with part_eq have "P x y".. moreover have "x ≠ y" proof assume "x = y" hence "PP y y" using ‹PP x y› by (rule subst) with proper_part_irreflexivity show "False".. qed ultimately show "P x y ∧ x ≠ y".. next assume rhs: "P x y ∧ x ≠ y" hence "x ≠ y".. from rhs have "P x y".. with part_eq have "PP x y ∨ x = y".. thus "PP x y" proof assume "PP x y" thus "PP x y". next assume "x = y" with ‹x ≠ y› show "PP x y".. qed qed show "P x x" proof - have "x = x" by (rule refl) hence "PP x x ∨ x = x".. with part_eq show "P x x".. qed show "O x y ⟷ (∃ z. P z x ∧ P z y)" using overlap_eq. show "P x y ⟹ P y x ⟹ x = y" proof - assume "P x y" assume "P y x" from part_eq have "PP x y ∨ x = y" using ‹P x y›.. thus "x = y" proof assume "PP x y" hence "¬ PP y x" by (rule proper_part_asymmetry) from part_eq have "PP y x ∨ y = x" using ‹P y x›.. thus "x = y" proof assume "PP y x" with ‹¬ PP y x› show "x = y".. next assume "y = x" thus "x = y".. qed qed qed show "P x y ⟹ P y z ⟹ P x z" proof - assume "P x y" assume "P y z" with part_eq have "PP y z ∨ y = z".. hence "PP x z ∨ x = z" proof assume "PP y z" from part_eq have "PP x y ∨ x = y" using ‹P x y›.. hence "PP x z" proof assume "PP x y" thus "PP x z" using ‹PP y z› by (rule proper_part_transitivity) next assume "x = y" thus "PP x z" using ‹PP y z› by (rule ssubst) qed thus "PP x z ∨ x = z".. next assume "y = z" moreover from part_eq have "PP x y ∨ x = y" using ‹P x y›.. ultimately show "PP x z ∨ x = z" by (rule subst) qed with part_eq show "P x z".. qed qed (*<*) end (*>*)