# Theory PM

section ‹ Introduction ›

(*<*)
theory PM
imports Main
begin
(*>*)

text ‹ In this paper, we use Isabelle/HOL to verify some elementary theorems and alternative axiomatizations
of classical extensional mereology, as well as some of its weaker subtheories.\footnote{For similar
developments see \<^cite>‹"sen_computational_2017"› and \<^cite>‹"bittner_formal_2018"›.} We mostly follow the
presentations from \<^cite>‹"simons_parts:_1987"›, \<^cite>‹"varzi_parts_1996"› and \<^cite>‹"casati_parts_1999"›,
with some important corrections from \<^cite>‹"pontow_note_2004"› and \<^cite>‹"hovda_what_2009"› as well as
some detailed proofs adapted from \<^cite>‹"pietruszczak_metamereology_2018"›.\footnote{For help with
this project I am grateful to Zach Barnett, Sam Baron, Bob Beddor, Olivier Danvy, Mark Goh,
Jeremiah Joven Joaquin, Wang-Yen Lee, Kee Wei Loo, Bruno Woltzenlogel Paleo, Michael Pelczar, Hsueh Qu,
Abelard Podgorski, Divyanshu Sharma, Manikaran Singh, Neil Sinhababu, Weng-Hong Tang and Zhang Jiang.} ›

text ‹ We will use the following notation throughout.\footnote{See \<^cite>‹"simons_parts:_1987"› pp. 99-100
for a helpful comparison of alternative notations.} ›

typedecl i
consts part :: "i ⇒ i ⇒ bool" ("P")
consts overlap :: "i ⇒ i ⇒ bool" ("O")
consts proper_part :: "i ⇒ i ⇒ bool" ("PP")
consts sum :: "i ⇒ i ⇒ i" (infix "⊕" 52)
consts product :: "i ⇒ i ⇒ i" (infix "⊗" 53)
consts difference :: "i ⇒ i ⇒ i" (infix "⊖" 51)
consts complement:: "i ⇒ i" ("─")
consts universe :: "i" ("u")
consts general_sum :: "(i ⇒ bool) ⇒ i" (binder "σ" 9)
consts general_product :: "(i ⇒ bool) ⇒ i" (binder "π" [8] 9)

section ‹ Premereology ›

text ‹ The theory of \emph{premereology} assumes parthood is reflexive and transitive.\footnote{
For discussion of reflexivity see \<^cite>‹"kearns_can_2011"›. For transitivity see \<^cite>‹"varzi_note_2006"›.}
In other words, parthood is assumed to be a partial ordering relation.\footnote{Hence the name \emph{premereology},
from \<^cite>‹"parsons_many_2014"› p. 6.} Overlap is defined as common parthood.\footnote{See
\<^cite>‹"simons_parts:_1987"› p. 28, \<^cite>‹"varzi_parts_1996"› p. 261 and \<^cite>‹"casati_parts_1999"› p. 36. } ›

locale PM =
assumes part_reflexivity: "P x x"
assumes part_transitivity : "P x y ⟹ P y z ⟹ P x z"
assumes overlap_eq: "O x y ⟷ (∃ z. P z x ∧ P z y)"
begin

subsection ‹ Parthood ›

lemma identity_implies_part : "x = y ⟹ P x y"
proof -
assume "x = y"
moreover have "P x x" by (rule part_reflexivity)
ultimately show "P x y" by (rule subst)
qed

subsection ‹ Overlap ›

lemma overlap_intro: "P z x ⟹ P z y ⟹ O x y"
proof-
assume "P z x"
moreover assume "P z y"
ultimately have "P z x ∧ P z y"..
hence "∃ z. P z x ∧ P z y"..
with overlap_eq show "O x y"..
qed

lemma part_implies_overlap: "P x y ⟹ O x y"
proof -
assume "P x y"
with part_reflexivity have "P x x ∧ P x y"..
hence "∃ z. P z x ∧ P z y"..
with overlap_eq show "O x y"..
qed

lemma overlap_reflexivity: "O x x"
proof -
have "P x x ∧ P x x" using part_reflexivity part_reflexivity..
hence "∃ z. P z x ∧ P z x"..
with overlap_eq show "O x x"..
qed

lemma overlap_symmetry: "O x y ⟹ O y x"
proof-
assume "O x y"
with overlap_eq have "∃ z. P z x ∧ P z y"..
hence "∃ z. P z y ∧ P z x" by auto
with overlap_eq show "O y x"..
qed

lemma overlap_monotonicity: "P x y ⟹ O z x ⟹ O z y"
proof -
assume "P x y"
assume "O z x"
with overlap_eq have "∃ v. P v z ∧ P v x"..
then obtain v where v: "P v z ∧ P v x"..
hence "P v z"..
moreover from v have "P v x"..
hence "P v y" using ‹P x y› by (rule part_transitivity)
ultimately have "P v z ∧ P v y"..
hence "∃ v. P v z ∧ P v y"..
with overlap_eq show "O z y"..
qed

text ‹ The next lemma is from \<^cite>‹"hovda_what_2009"› p. 66. ›

lemma overlap_lemma: "∃x. (P x y ∧ O z x) ⟶ O y z"
proof -
fix x
have "P x y ∧ O z x ⟶ O y z"
proof
assume antecedent: "P x y ∧ O z x"
hence "O z x"..
with overlap_eq have "∃v. P v z ∧ P v x"..
then obtain v where v: "P v z ∧ P v x"..
hence "P v x"..
moreover from antecedent have "P x y"..
ultimately have "P v y" by (rule part_transitivity)
moreover from v have "P v z"..
ultimately have "P v y ∧ P v z"..
hence "∃v. P v y ∧ P v z"..
with overlap_eq show "O y z"..
qed
thus "∃x. (P x y ∧ O z x) ⟶ O y z"..
qed

subsection ‹ Disjointness ›

lemma disjoint_implies_distinct: "¬ O x y ⟹ x ≠ y"
proof -
assume "¬ O x y"
show "x ≠ y"
proof
assume "x = y"
hence "¬ O y y" using ‹¬ O x y› by (rule subst)
thus "False" using overlap_reflexivity..
qed
qed

lemma disjoint_implies_not_part: "¬ O x y ⟹ ¬ P x y"
proof -
assume "¬ O x y"
show "¬ P x y"
proof
assume "P x y"
hence "O x y" by (rule part_implies_overlap)
with ‹¬ O x y› show "False"..
qed
qed

lemma disjoint_symmetry: "¬ O x y ⟹ ¬ O y x"
proof -
assume "¬ O x y"
show "¬ O y x"
proof
assume "O y x"
hence "O x y" by (rule overlap_symmetry)
with ‹¬ O x y› show "False"..
qed
qed

lemma disjoint_demonotonicity: "P x y ⟹ ¬ O z y ⟹ ¬ O z x"
proof -
assume "P x y"
assume "¬ O z y"
show "¬ O z x"
proof
assume "O z x"
with ‹P x y› have "O z y"
by (rule overlap_monotonicity)
with ‹¬ O z y› show "False"..
qed
qed

end

(*<*)end(*>*)