I am stuck with a simple problem in mereology (the theory of parthood), where $P x y$ stands for $x$ is part of $y$ and $O x y$ stands for $x$ and $y$ overlap. From the axiom schema $(\exists x) \phi x \rightarrow (\exists z)(\forall y)(O y z \leftrightarrow (\exists x)(\phi x \wedge O y x))$, known as fusion or unrestricted composition, I am trying to derive the following, known as the sum and product axioms respectively:
$(\exists z) (Pxz \wedge Pyz) \rightarrow (\exists z) (\forall w)(O w z \leftrightarrow (O w x \vee O w y))$
$(\exists z) (Pzx \wedge Pzy) \rightarrow (\exists z) (\forall w) (P w z \leftrightarrow (Pwx \wedge Pwy))$.
I suppose it should be obvious, but what substitutions should I use for $\phi$?
It's assumed that $P$ is reflexive, antisymmetric and transitive, and that $O x y \leftrightarrow (\exists z)(P z x \wedge P z y)$. I shouldn't need to use the axiom of strong supplementation, $\neg P y x \to (\exists z) (P z y \wedge \neg O z x)$. But an answer which does use this axiom would be very helpful too.
The formulations are from Achille Varzi and Roberto Casati's Parts and Places (Cambridge, Mass: MIT Press, 1999), pp. 33-47. See also https://plato.stanford.edu/entries/mereology/
To answer my own question, to prove the sum axiom, let $\phi x$ be $x = a \vee x = b$. Then we have:
$(\exists x) (x = a \vee x = b) \rightarrow (\exists z)(\forall y)(O y z \leftrightarrow ((x = a \vee x = b) \wedge O y x))$
$(\exists z)(\forall y)(O y z \leftrightarrow ((x = a \vee x = b) \wedge O y x))$ from (1), because the antecedent is a tautology.
$(\exists z)(\forall y)(O y z \leftrightarrow (O a y \vee O by))$ from (2), since $(x = a \vee x = b) \wedge O y x)$ implies $Oya \vee Oyb$.
And this is the same as the sum axiom, except with different letters.
For the second question, let $\phi x$ be $P x a \wedge P x b$. Then we have:
which says that if $a$ and $b$ overlap there is a sum of all the things that are part of both of them. The problem is then just to show that this sum is also the product of $a$ and $b$. But doing this does require strong supplementation.
The proof turns out to be quite lengthy, but can be found in [1] p. 204, which also notes that the claim that the claim that the product axiom can be derived from weak supplementation alone is a common misconception in the literature.
[1] Carsten Pontow (2004) "A note on axiomatic theories of parthood" Data and Knowledge Engineering 50(2): 195-213.