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