Theory EM

section ‹ Extensional Mereology ›

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

text ‹ Extensional mereology adds to ground mereology the axiom of strong supplementation.\footnote{
See \<^cite>‹"simons_parts:_1987"› p. 29, \<^cite>‹"varzi_parts_1996"› p. 262 and \<^cite>‹"casati_parts_1999"› 
p. 39-40.} ›

locale EM = M +
  assumes strong_supplementation: 
    "¬ P x y ⟹ (∃z. P z x ∧ ¬ O z y)"
begin

text ‹ Strong supplementation entails weak supplementation.\footnote{See \<^cite>‹"simons_parts:_1987"›
p. 29 and \<^cite>‹"casati_parts_1999"› p. 40.} ›

lemma weak_supplementation: "PP x y ⟹ (∃z. P z y ∧ ¬ O z x)"
proof -
  assume "PP x y"
  hence "¬ P y x" by (rule proper_implies_not_part)
  thus "∃z. P z y ∧ ¬ O z x" by (rule strong_supplementation)
qed

end

text ‹ So minimal mereology is a subtheory of extensional mereology.\footnote{\<^cite>‹"casati_parts_1999"› p. 40.} ›

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

text ‹ Strong supplementation also entails the proper parts principle.\footnote{See \<^cite>‹"simons_parts:_1987"›
pp. 28-9 and \<^cite>‹"varzi_parts_1996"› p. 263.} ›

context EM
begin

lemma proper_parts_principle:
"(∃z. PP z x) ⟹ (∀z. PP z x ⟶ P z y) ⟹ P x y"
proof -
  assume "∃z. PP z x"
  then obtain v where v: "PP v x"..
  hence "P v x" by (rule proper_implies_part)
  assume antecedent: "∀z. PP z x ⟶ P z y"
  hence "PP v x ⟶ P v y"..
  hence "P v y" using ‹PP v x›..
  with ‹P v x› have "P v x ∧ P v y"..
  hence "∃v. P v x ∧ P v y"..
  with overlap_eq have "O x y"..
  show "P x y"
  proof (rule ccontr)
    assume "¬ P x y"
    hence "∃z. P z x ∧ ¬ O z y"
      by (rule strong_supplementation)
    then obtain z where z: "P z x ∧ ¬ O z y"..
    hence "P z x"..
    moreover have "z ≠ x"
    proof
      assume "z = x"
      moreover from z have "¬ O z y"..
      ultimately have "¬ O x y" by (rule subst)
      thus "False"  using ‹O x y›..
    qed
    ultimately have "P z x ∧ z ≠ x"..
    with nip_eq have "PP z x"..
    from antecedent have "PP z x ⟶ P z y"..
    hence "P z y" using ‹PP z x›..
    hence "O z y" by (rule part_implies_overlap)
    from z have "¬ O z y"..
    thus "False" using ‹O z y›..
  qed
qed

text ‹ Which with antisymmetry entails the extensionality of proper parthood.\footnote{See
\<^cite>‹"simons_parts:_1987"› p. 28, \<^cite>‹"varzi_parts_1996"› p. 263 and \<^cite>‹"casati_parts_1999"›
p. 40.} ›

theorem proper_part_extensionality:
"(∃z. PP z x ∨ PP z y) ⟹ x = y ⟷ (∀z. PP z x ⟷ PP z y)"
proof -
  assume antecedent: "∃z. PP z x ∨ PP z y"
  show "x = y ⟷ (∀z. PP z x ⟷ PP z y)"
  proof
    assume "x = y"
    moreover have "∀z. PP z x ⟷ PP z x" by simp
    ultimately show "∀z. PP z x ⟷ PP z y" by (rule subst)
  next
    assume right: "∀z. PP z x ⟷ PP z y"
    have "∀z. PP z x ⟶ P z y"
    proof
      fix z
      show "PP z x ⟶ P z y"
      proof
        assume "PP z x"
        from right have "PP z x ⟷ PP z y"..
        hence "PP z y" using ‹PP z x›..
        thus "P z y" by (rule proper_implies_part)
      qed
    qed
    have "∀z. PP z y ⟶ P z x"
    proof
      fix z
      show "PP z y ⟶ P z x"
      proof
        assume "PP z y"
        from right have "PP z x ⟷ PP z y"..
        hence "PP z x" using ‹PP z y›..
        thus "P z x" by (rule proper_implies_part)
      qed
    qed
    from antecedent obtain z where z: "PP z x ∨ PP z y"..
    thus "x = y"
    proof (rule disjE)
      assume "PP z x"
      hence "∃z. PP z x"..
      hence "P x y" using ‹∀z. PP z x ⟶ P z y›
        by (rule proper_parts_principle)
      from right have "PP z x ⟷ PP z y"..
      hence "PP z y" using ‹PP z x›..
      hence "∃z. PP z y"..
      hence "P y x" using ‹∀z. PP z y ⟶ P z x›
        by (rule proper_parts_principle)
      with ‹P x y› show "x = y"
        by (rule part_antisymmetry)
    next
      assume "PP z y"
      hence "∃z. PP z y"..
      hence "P y x" using ‹∀z. PP z y ⟶ P z x›
        by (rule proper_parts_principle)
      from right have "PP z x ⟷ PP z y"..
      hence "PP z x" using ‹PP z y›..
      hence "∃z. PP z x"..
      hence "P x y" using ‹∀z. PP z x ⟶ P z y›
          by (rule proper_parts_principle)
      thus "x = y"
        using ‹P y x› by (rule part_antisymmetry)
    qed
  qed
qed

text ‹ It also follows from strong supplementation that parthood is definable in terms of overlap.\footnote{
See \<^cite>‹"parsons_many_2014"› p. 4.}  ›

lemma part_overlap_eq: "P x y ⟷ (∀z. O z x ⟶ O z y)"
proof
  assume "P x y"
  show "(∀z. O z x ⟶ O z y)"
  proof
    fix z
    show "O z x ⟶ O z y"
    proof
      assume "O z x"
      with ‹P x y› show "O z y"
        by (rule overlap_monotonicity)
    qed
  qed
next
  assume right: "∀z. O z x ⟶ O z y"
  show "P x y"
  proof (rule ccontr)
    assume "¬ P x y"
    hence "∃z. P z x ∧ ¬ O z y"
      by (rule strong_supplementation)
    then obtain z where z: "P z x ∧ ¬ O z y"..
    hence "¬ O z y"..
    from right have "O z x ⟶ O z y"..
    moreover from z have "P z x"..
    hence "O z x" by (rule part_implies_overlap)
    ultimately have "O z y"..
    with ‹¬ O z y› show "False"..
  qed
qed

text ‹ Which entails the extensionality of overlap. ›

theorem overlap_extensionality: "x = y ⟷ (∀z. O z x ⟷ O z y)"
proof
  assume "x = y"
  moreover have "∀z. O z x ⟷ O z x"
  proof
    fix z
    show "O z x ⟷ O z x"..
  qed
  ultimately show "∀z. O z x ⟷ O z y"
    by (rule subst)
next
  assume right: "∀z. O z x ⟷ O z y"
  have "∀z. O z y ⟶ O z x"
  proof
    fix z
    from right have "O z x ⟷ O z y"..
    thus "O z y ⟶ O z x"..
  qed
  with part_overlap_eq have "P y x"..
  have "∀z. O z x ⟶ O z y"
  proof
    fix z
    from right have "O z x ⟷ O z y"..
    thus "O z x ⟶ O z y"..
  qed
  with part_overlap_eq have "P x y"..
  thus "x = y" 
    using ‹P y x› by (rule part_antisymmetry)
qed

end

(*<*) end (*>*)