Theory GMM

section ‹ General Minimal Mereology ›

theory GMM
 imports GM MM

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

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