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