Showing $\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle \implies \langle \exists y: P.y : Q.y \rangle $ is a theorem. A possible proof using a Natural Deduction system like Fitch is not difficult. But, I would like to prove it using Equational Logic. This system uses common rules of propositional logic like DeMorgan, etc..., and Predicate logic rules used in books like:

*

*A Logical Approach to Discrete Math (David Gries).

*

*Complete book can be found here: https://link.springer.com/book/10.1007/978-1-4757-3837-7

*List of rules on page 503.



*Programming in the 1990s (Edward Cohen).

My proof starts as follows:
I assume the antecedent holds $$\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle$$ and try to reach $$\langle \exists x:: P.x \land Q.x \rangle$$
Attempted proof:
$$
\begin{align*}
  & \langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle\\
  \implies & \{\text{Instantiation } (\forall)\}\\
  & P.a \land \langle \exists x:: Q.x \rangle \\
  \equiv & \{\text{Distributivity of} \land \text{over} \exists \} \\
  & \langle \exists x:: P.a \land Q.x \rangle 
\end{align*}
$$
Of course, the proof is not complete. Does someone know if this proof is possible in this context ?
 A: When creating a formal proof for a logical implication, it helps to reason about it intuitively first.
This can also help reveal if a partial proof you are working on leads to a dead end.
For example, your partial proof reads intuitively as:

If all $x$ have property $P.x$ and there is some $x$ with property $Q.x$, then there must be some $x$ with property $P.x\land Q.x$: indeed, let $a$ be an arbitrary object, then we know it has property $P.a$. Since there is some $x$ with property $Q.x$, we can conclude that there is some $x$ with $P.a\land Q.x$... but now what?

This reveals that it was probably not the best idea to instantiate the universal quantifier first, but rather the existential quantifier:

If all $x$ have property $P.x$ and there is some $x$ with property $Q.x$, then there must be some $x$ with the property $P.x\land Q.x$: indeed, say the object with property $Q$ is called $a$ (so that $Q.a$), then since all $x$ have property $P.x$, then especially $a$ must have property $P.a$. Combining this with the fact that $a$ has property $Q.a$, we can conclude that $a$ has property $P.a\land Q.a$. In particular, there is some $x$ with $P.x\land Q.x$.

Writing this out formally using natural deduction would look like this:

*

*$\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (assumption for implication intro)

*$\langle \exists x :: Q.x\rangle$ (conjunction elim, 1)
2.1 $Q.a$ (assumption for existential elim)
2.2 $\langle \forall x :: P.x\rangle$ (conjunction elim, 1)
2.3 $P.a$ (universal elim, 2.2)
2.4 $P.a\land Q.a$ (conjunction intro, 2.1, 2.3)
2.5 $\langle \exists x :: P.x\land Q.x\rangle$ (existential intro, 2.4)

*$\langle \exists x :: P.x\land Q.x\rangle$ (existential elim, 2, 2.1-2.5)

from which we conclude $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle \implies \langle \exists x :: P.x\land Q.x\rangle$ by implication intro on 1-3.
This argument guides how to produce an axiomatic argument. The main trick in this case is that an existential intro is sidestepped by reasoning towards wrapping the entire argument in the existential quantifier. You can then reason within the scope of an existential quantifier just as though it wasn't there.
(antecedent) $\langle \forall x :: P.x\rangle\land\langle\exists x :: Q.x\rangle$
$\equiv$ $\langle \forall y :: P.y\rangle\land\langle\exists x :: Q.x\rangle$ (change of variables)
$\equiv$ $\langle \exists x :: \langle \forall y :: P.y\rangle \land Q.x\rangle$ (distributivity of $\land$ over $\exists$; this wraps the whole statement in $\exists$)
$\implies$ $\langle \exists x :: P.x \land Q.x \rangle$  (instantiation of $\forall$ at $x$)
A: The trick would be to instantiate specifically to the witness for the existental.
$${\langle\forall x::P.x\rangle\land\langle\exists x::Q.x\rangle\\\Downarrow~\\\langle\exists x:Q.x:P.x\rangle\land\langle\exists x::Q.x\rangle}$$
