# Theory M

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