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