Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
I need to prove that using natural deduction in tree format
$(\forall x\ p(x)\to \neg q(x)) \vdash \neg (\exists x (p(x)\land q(x)))$
I have built the following proof which is incomplete and I do not know if is correct. Can some of you help me to figure out what can I do next?
Before formalizing the proof, write it in an informal way. To prove that $\lnot \exists x (p(x) \land q(x))$ from the hypothesis $\forall x (p(x) \to \lnot q(x))$, you can show that if you further assume that $\exists x (p(x) \land q(y))$ you get a contradiction. Let's find this contradiction!
From $\exists x (p(x) \land q(y))$ we know that there is some $y$ such that $p(y)$ and $q(y)$. But from the hypothesis $\forall x (p(x) \to \lnot q(x))$, we know that in particular for $x = y$ we have $p(y) \to \lnot q(y)$. By modus ponens, from $p(y) \to \lnot q(y)$ and $p(y)$ it follows that $\lnot q(x)$, which contradicts $q(y)$ inferred from $\exists x (p(x) \land q(y))$. Absurd.
The informal argument above can be formalized in natural deduction as follows:
\begin{align} \small \dfrac{\dfrac{[\exists x (p(x) \land q(x))]^* \quad \dfrac{ \dfrac{\dfrac{\forall x (p(y) \to \lnot q(y))}{p(y) \to \lnot q(y)}\forall_\text{elim} \quad \dfrac{[p(y) \land q(y)]^{**}}{p(y)}\land_\text{elim}}{\lnot q(y)}\to_\text{elim} \quad \dfrac{[p(y) \land q(y)]^{**}}{q(y)}\land_\text{elim}}{\bot}\lnot_\text{elim}}{\bot}\exists_\text{elim}^{**}}{\lnot \,\exists x (p(x) \land q(x))}\lnot_\text{intro}^* \end{align} where I marked with $*$ and $**$ the discharged assumptions.
In your attempt, you have translated the formula on the RHS of $\vdash$ to $\forall x \lnot (p(x) \land q(x))$, which is clearly logical equivalent to $\lnot \exists x (p(x) \land q(x))$. However, in this kind of exercises about natural deduction, usually you are not allowed to substitute a formula with a logically equivalent one, unless you have already proved their equivalence using natural deduction. The rationale is that these exercises are intended to make you familiar with natural deduction, so if you were entitled to substitute a formula with an equivalent one without proving that in natural deduction, the spirit and the aim of the exercise would be lost.
