Deduction of $\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))$

Question

I trying to study for my final exam and I can't figure out how to solve this:

$\forall x(\neg p(x)\rightarrow q(x)), \forall z(p(z)\rightarrow r(z))\vdash \forall z(\neg r(z) \rightarrow\exists yq(y))$

This is what I have so far:

1. $\forall x(\neg p(x)\rightarrow q(x))$
2. $\forall z(\neg p(z)\rightarrow r(z))$
3. $p(x_0)\rightarrow q(x_0)$ (using 1 and UE($S^x_{x_0}$))
4. $p(x_0)\rightarrow r(x_0)$ (using 2 and UE($S^z_{x_0}$))
5. $\neg p(x_0)\rightarrow r(x_0)$ (using 3, 4 and Hypothetical syllogism)
6. $r(x_0) \vee q(x_0)$ (using 5)
7. $\neg r(x_0) \rightarrow q(x_0)$ (using 6)
8. $\forall z(\neg r(z)\rightarrow q(z))$ (using Universal Introduction)

But I can't reach $\forall z(\neg r(z) \rightarrow\exists yq(y))$

I can't find any theorem that I can use to put the $\exists$ in the middle of the $\forall$.

Can anyone help me?

Thank you

Answer 1

Your proof attempts to use Hypothetical Syllogism immediately after the two Universal Eliminations.

Before you can do that, you will need to use Contraposition, to get two conditionals in the correct form:

$$\lnot r(c)\to \lnot p(c)~,~\lnot p(c)\to q(c)~\vdash~\lnot r(c)\to q(c)$$

So that just leaves you with the steps to derive the required conditional from that.

$$\def\fitch#1#2{\quad\begin{array}{|l} #1\\\hline #2\end{array}} \fitch{~1.~\forall x~(\lnot p(x)\to q(x))\hspace{5.5ex}\text{Premise}\\~2.~\forall z~(p(z)\to r(z))\hspace{8ex}\text{Premise}}{\fitch{~3.~[~c~]\hspace{17.5ex}\text{Assumption}}{~4.~\lnot p(c)\to q(c)\hspace{8ex}\forall\text{E},1,3\\~5.~p(c)\to r(c)\hspace{9.5ex}\forall\text{E},2,3\\~6.~\lnot r(c)\to\lnot p(c)\hspace{6.5ex}\text{Contraposition},5\\~7.~\lnot r(c)\to q(c)\hspace{8ex}\text{Hypothetical Syllogism},6,4\\{\small\fitch{~8.~\ldots}{~9.~\ldots\\10.~\ldots}}\\11.~\lnot r(c)\to\exists y~q(y)\hspace{3.5ex}\to\!\text{I},8{-}10}\\12.~\forall z~(\lnot r(z)\to \exists y~q(y))\hspace{3ex}\forall\text{I},3{-}11}$$

Answer 2

Your attempt so far is very sloppy:

• (2) has a negation that shouldn't be there,
• (5) does not follow since the consequent in (3) is $q(x_0)$ and the antecedent in (4) is $p(x_0)$,
• (6) does not at all follow from (5).

I would take a lot more care with these proofs, both in not making mistakes such as above, and in annotating which rules you use (instead of just "using").

---

Here is a proof:

\begin{align} 1.&\quad \forall x(\lnot p(x)\to q(x))&& \text{(assumption)}\\ 2.&\quad \forall x(p(x)\to r(x))&& \text{(assumption)}\\ 3.&\quad \lnot p(t)\to q(t) && \text{(universal elimination on 1.)}\\ 4.&\quad p(t)\to r(t) && \text{(universal elimination on 2.)}\\ 5.&\quad \lnot q(t)\to \lnot\lnot p(t) && \text{(contraposition on 3.)}\\ 6.&\quad \lnot\lnot p(t)\to p(t) && \text{(double negation elimination)}\\ 7.&\quad \lnot q(t)\to p(t) && \text{(hypothetical syllogism on 5. and 6.)}\\ 8.&\quad \lnot q(t)\to r(t) && \text{(hypothetical syllogism on 7. and 4.)}\\ 9.&\quad \lnot r(t)\to \lnot\lnot q(t) && \text{(contraposition on 8.)}\\ 10.&\quad \lnot\lnot q(t)\to q(t) && \text{(double negation elimination)}\\ 11.&\quad \lnot r(t)\to q(t) && \text{(hypothetical syllogism on 9. and 10.)}\\ 12.&\quad q(t)\to \exists y\,q(y) && \text{(existential introduction)}\\ 13.&\quad \lnot r(t)\to \exists y\,q(y) && \text{(hypothetical syllogism on 11. and 12.)}\\ 14.&\quad \forall x(\lnot r(x)\to\exists y\,q(y)) && \text{(universal introduction on 13.)}\\ \end{align}

Note that in step $14.$ you need to ascertain that $t$ is not a free variable in any of the assumptions ($1.$ and $2.$) and $x$ is not free in formula $13.$

I doubt that "hypothetical syllogism" and "contraposition" are actual derivation rules you are allowed to use, but instead are shortcuts. Similarly I'm not sure if "double negation elimination" and "existential introduction" are axiom schemes that could be used.

To be completely correct, you will have to also show that these shortcuts / theorems can be derived using just the axioms and derivation rules native to your proof system (I don't know which specific system you work with, so I cannot give you a proof of those).