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