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