# Theory MM

section ‹ Minimal Mereology ›

(*<*)
theory MM
imports M
begin
(*>*)

text ‹ Minimal mereology adds to ground mereology the axiom of weak supplementation.\footnote{
See \<^cite>‹"varzi_parts_1996"› and \<^cite>‹"casati_parts_1999"› p. 39. The name \emph{minimal mereology}
reflects the, controversial, idea that weak supplementation is analytic. See, for example, \<^cite>‹"simons_parts:_1987"›
p. 116, \<^cite>‹"varzi_extensionality_2008"› p. 110-1, and \<^cite>‹"cotnoir_is_2018"›. For general
discussion of weak supplementation see, for example \<^cite>‹"smith_mereology_2009"› pp. 507 and
\<^cite>‹"donnelly_using_2011"›.} ›

locale MM = M +
assumes weak_supplementation: "PP y x ⟹ (∃ z. P z x ∧ ¬ O z y)"

text ‹ The rest of this section considers three alternative axiomatizations of minimal mereology. The
first alternative axiomatization replaces improper with proper parthood in the consequent of weak
supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 28.} ›

locale MM1 = M +
assumes proper_weak_supplementation:
"PP y x ⟹ (∃ z. PP z x ∧ ¬ O z y)"

sublocale MM ⊆ MM1
proof
fix x y
show "PP y x ⟹ (∃ z. PP z x ∧ ¬ O z y)"
proof -
assume "PP y x"
hence "∃ z. P z x ∧ ¬ O z y" by (rule weak_supplementation)
then obtain z where z: "P z x ∧ ¬ O z y"..
hence "¬ O z y"..
from z have "P z x"..
hence "P z x ∧ z ≠ x"
proof
show "z ≠ x"
proof
assume "z = x"
hence "PP y z"
using ‹PP y x› by (rule ssubst)
hence "O y z" by (rule proper_implies_overlap)
hence "O z y" by (rule overlap_symmetry)
with ‹¬ O z y› show "False"..
qed
qed
with nip_eq have "PP z x"..
hence "PP z x ∧ ¬ O z y"
using ‹¬ O z y›..
thus "∃ z. PP z x ∧ ¬ O z y"..
qed
qed

sublocale MM1 ⊆ MM
proof
fix x y
show weak_supplementation: "PP y x ⟹ (∃ z. P z x ∧ ¬ O z y)"
proof -
assume "PP y x"
hence "∃ z. PP z x ∧ ¬ O z y" by (rule proper_weak_supplementation)
then obtain z where z: "PP z x ∧ ¬ O z y"..
hence "PP z x"..
hence "P z x" by (rule proper_implies_part)
moreover from z have "¬ O z y"..
ultimately have "P z x ∧ ¬ O z y"..
thus "∃ z. P z x ∧ ¬ O z y"..
qed
qed

text ‹ The following two corollaries are sometimes found in the literature.\footnote{See \<^cite>‹"simons_parts:_1987"› p. 27. For the names \emph{weak company}
and \emph{strong company} see \<^cite>‹"cotnoir_non-wellfounded_2012"› p. 192-3 and \<^cite>‹"varzi_mereology_2016"›.} ›

context MM
begin

corollary weak_company: "PP y x ⟹ (∃ z. PP z x ∧ z ≠ y)"
proof -
assume "PP y x"
hence "∃ z. PP z x ∧ ¬ O z y" by (rule proper_weak_supplementation)
then obtain z where z: "PP z x ∧ ¬ O z y"..
hence "PP z x"..
from z have "¬ O z y"..
hence "z ≠ y" by (rule disjoint_implies_distinct)
with ‹PP z x› have "PP z x ∧ z ≠ y"..
thus "∃ z. PP z x ∧ z ≠ y"..
qed

corollary strong_company: "PP y x ⟹ (∃ z. PP z x ∧ ¬ P z y)"
proof -
assume "PP y x"
hence "∃z. PP z x ∧ ¬ O z y" by (rule proper_weak_supplementation)
then obtain z where z: "PP z x ∧ ¬ O z y"..
hence "PP z x"..
from z have "¬ O z y"..
hence "¬ P z y" by (rule disjoint_implies_not_part)
with ‹PP z x› have  "PP z x ∧ ¬ P z y"..
thus "∃ z. PP z x ∧ ¬ P z y"..
qed

end

text ‹ If weak supplementation is formulated in terms of nonidentical parthood, then the antisymmetry
of parthood is redundant, and we have the second alternative axiomatization of minimal mereology.\footnote{
See \<^cite>‹"cotnoir_antisymmetry_2010"› p. 399, \<^cite>‹"donnelly_using_2011"› p. 232,
\<^cite>‹"cotnoir_non-wellfounded_2012"› p. 193 and \<^cite>‹"obojska_remarks_2013"› pp. 235-6.} ›

locale MM2 = PM +
assumes nip_eq: "PP x y ⟷ P x y ∧ x ≠ y"
assumes weak_supplementation: "PP y x ⟹ (∃ z. P z x ∧ ¬ O z y)"

sublocale MM2 ⊆ MM
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"
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"..
hence "∃ z. P z y ∧ ¬ O z x" by (rule weak_supplementation)
then obtain z where z: "P z y ∧ ¬ O z x"..
hence "¬ O z x"..
hence "¬ P z x" by (rule disjoint_implies_not_part)
from z have "P z y"..
hence "P z x" using ‹P y x› by (rule part_transitivity)
with ‹¬ P z x› show "False"..
qed
qed
show "PP y x ⟹ ∃z. P z x ∧ ¬ O z y" using weak_supplementation.
qed

sublocale MM ⊆ MM2
proof
fix x y
show "PP x y ⟷ (P x y ∧ x ≠ y)" using nip_eq.
show "PP y x ⟹ ∃z. P z x ∧ ¬ O z y" using weak_supplementation.
qed

text ‹ Likewise, if proper parthood is adopted as primitive, then the asymmetry of proper parthood
is redundant in the context of weak supplementation, leading to the third alternative
axiomatization.\footnote{See \<^cite>‹"donnelly_using_2011"› p. 232 and \<^cite>‹"cotnoir_is_2018"›.} ›

locale MM3 =
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_transitivity: "PP x y ⟹ PP y z ⟹ PP x z"
assumes weak_supplementation: "PP y x ⟹ (∃ z. P z x ∧ ¬ O z y)"
begin

lemma part_reflexivity: "P x x"
proof -
have "x = x"..
hence "PP x x ∨ x = x"..
with part_eq show "P x x"..
qed

lemma proper_part_irreflexivity: "¬ PP x x"
proof
assume "PP x x"
hence "∃ z. P z x ∧ ¬ O z x" by (rule weak_supplementation)
then obtain z where z: "P z x ∧ ¬ O z x"..
hence "¬ O z x"..
from z have "P z x"..
with part_reflexivity have "P z z ∧ P z x"..
hence "∃ v. P v z ∧ P v x"..
with overlap_eq have "O z x"..
with ‹¬ O z x› show "False"..
qed

end

sublocale MM3 ⊆ M4
proof
fix x y z
show "P x y ⟷ PP x y ∨ x = y" using part_eq.
show "O x y ⟷ (∃ z. P z x ∧ P z y)" using overlap_eq.
show proper_part_irreflexivity: "PP x y ⟹ ¬ PP y x"
proof -
assume "PP x y"
show "¬ PP y x"
proof
assume "PP y x"
hence "PP y y" using ‹PP x y› by (rule proper_part_transitivity)
with proper_part_irreflexivity show "False"..
qed
qed
show "PP x y ⟹ PP y z ⟹ PP x z" using proper_part_transitivity.
qed

sublocale MM3 ⊆ MM
proof
fix x y
show "PP y x ⟹ (∃ z. P z x ∧ ¬ O z y)" using weak_supplementation.
qed

sublocale MM ⊆ MM3
proof
fix x y z
show "P x y ⟷ (PP x y ∨ x = y)" using part_eq.
show "O x y ⟷ (∃z. P z x ∧ P z y)" using overlap_eq.
show "PP x y ⟹ PP y z ⟹ PP x z" using proper_part_transitivity.
show "PP y x ⟹ ∃z. P z x ∧ ¬ O z y" using weak_supplementation.
qed

(*<*) end (*>*)