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