# Theory GM

section ‹ General Mereology ›

(*<*)
theory GM
imports CM
begin (*>*)

text ‹ The theory of \emph{general mereology} adds the axiom of fusion to ground mereology.\footnote{
See cite"simons_parts:_1987" p. 36, cite"varzi_parts_1996" p. 265 and cite"casati_parts_1999" p. 46.} ›

locale GM = M +
assumes fusion:
" x. φ x   z.  y. O y z  ( x. φ x  O y x)"
begin

text ‹ Fusion entails sum closure. ›

theorem sum_closure: " z.  w. O w z  (O w a  O w b)"
proof -
have "a = a"..
hence "a = a  a = b"..
hence " x. x = a  x = b"..
hence "( z.  y. O y z  ( x. (x = a  x = b)  O y x))"
by (rule fusion)
then obtain z where z:
" y. O y z  ( x. (x = a  x = b)  O y x)"..
have " w. O w z  (O w a  O w b)"
proof
fix w
from z have w: "O w z  ( x. (x = a  x = b)  O w x)"..
show "O w z  (O w a  O w b)"
proof
assume "O w z"
with w have " x. (x = a  x = b)  O w x"..
then obtain x where x: "(x = a  x = b)  O w x"..
hence "O w x"..
from x have "x = a  x = b"..
thus "O w a  O w b"
proof (rule disjE)
assume "x = a"
hence "O w a" using O w x by (rule subst)
thus "O w a  O w b"..
next
assume "x = b"
hence "O w b" using O w x by (rule subst)
thus "O w a  O w b"..
qed
next
assume "O w a  O w b"
hence " x. (x = a  x = b)  O w x"
proof (rule disjE)
assume "O w a"
with a = a  a = b have "(a = a  a = b)  O w a"..
thus " x. (x = a  x = b)  O w x"..
next
have "b = b"..
hence "b = a  b = b"..
moreover assume "O w b"
ultimately have "(b = a  b = b)  O w b"..
thus " x. (x = a  x = b)  O w x"..
qed
with w show "O w z"..
qed
qed
thus " z.  w. O w z  (O w a  O w b)"..
qed

end

(*<*) end (*>*)