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