Theory GMM

section ‹ General Minimal Mereology ›

(*<*)
theory GMM
 imports GM MM
begin
(*>*)

text ‹ The theory of \emph{general minimal mereology} adds general mereology to minimal mereology.\footnote{
See \<^cite>‹"casati_parts_1999"› p. 46.} ›

locale GMM = GM + MM
begin

text ‹ It is natural to assume that just as closed minimal mereology and closed extensional mereology
are the same theory, so are general minimal mereology and general extensional mereology.\footnote{For
this mistake see \<^cite>‹"simons_parts:_1987"› p. 37 and \<^cite>‹"casati_parts_1999"› p. 46. The mistake
is corrected in \<^cite>‹"pontow_note_2004"› and \<^cite>‹"hovda_what_2009"›. For discussion of the significance
of this issue see, for example, \<^cite>‹"varzi_universalism_2009"› and \<^cite>‹"cotnoir_does_2016"›.}
But this is not the case, since the proof of strong supplementation in closed minimal mereology
required the product closure axiom. However, in general minimal mereology, the fusion axiom does not 
entail the product closure axiom. So neither product closure nor strong supplementation are theorems. ›

lemma product_closure: 
  "O x y ⟹ (∃ z. ∀ v. P v z ⟷ P v x ∧ P v y)" 
  nitpick [expect = genuine] oops

lemma strong_supplementation: "¬ P x y ⟹ (∃ z. P z x ∧ ¬ O z y)"
  nitpick [expect = genuine] oops

end

(*<*) end (*>*)