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 ?
Best Answer
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:
This reveals that it was probably not the best idea to instantiate the universal quantifier first, but rather the existential quantifier:
Writing this out formally using natural deduction would look like this:
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)
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$)