Predicate logic problem using natural deduction

Question

I have the following clauses:

$1. \forall x ({Ax \rightarrow Bx})$

$2. \forall x (({{Cx \wedge Bx }) \rightarrow Dx})$

$3. \forall x \exists y ({Cy \wedge Ryx})$

$4. \forall x \forall y ({({Ryx \wedge Dy }) \rightarrow Dx})$

And I need to prove:

$\forall x (({{ \forall y ({Ryx \rightarrow Ay })}) \rightarrow Dx})$

Using natural deduction.

I've tried to manipulate #4 but could not get it to look like the expected clause. Any clue is appericiated.

Answer 1

$$\newcommand{\DeductionBox} [1]{\begin{array} {l|} #1 \\ \hline \end{array}}$$

The basic idea of the proof is, loosely:

for a free x, there is a set of ys satisfying Ryx
for all of those ys, Ay holds by assumption, and thus By holds
for at least one of those ys
  Cy holds
  so for that y, Dy holds 
If Dy holds for some y, then Dx holds for the y

$$\begin{array} {l} \begin{array} {rlr} (1) & \forall \langle x,~ Ax \implies Bx \rangle & \text{Given} \\ (2) & \forall \langle x,~ Bx \land Cx \implies Dx \rangle & \text{Given} \\ (3) & \forall \langle x,~ \exists \langle y,~ Cy \land Ryx \rangle ~ \rangle & \text{Given} \\ (4) & \forall \langle x,~ \forall \langle y,~ Ryx \land Dy \implies Dx \rangle ~ \rangle & \text{Given} \\ \end{array}\\ \\ \DeductionBox{ \begin{array} {rlr} \quad (5) & \forall \langle y,~ Ryx \implies Ay \rangle & \text{New Assumption} \\ \end{array} \\ \\ \DeductionBox{ \begin{array} {rlr} \quad \quad (6) & Cy \land Ryx & \text{New Assumption} \\ \quad \quad (7) & Ryx & \land-\text{Elimination of }(6) \\ \quad \quad (8) & Ryx \implies Ay & \forall-\text{Elimination of }(5) \\ \quad \quad (9) & Ay & \text{Modus Ponens of }(7) \text{ and } (8) \\ \quad \quad (10) & Ay \implies By & \forall-\text{Elimination of }(1) \\ \quad \quad (11) & By & \text{Modus Ponens of }(9) \text{ and } (10) \\ \quad \quad (12) & Cy & \land-\text{Elimination of }(6) \\ \quad \quad (13) & By \land Cy & \land-\text{Introduction of }(11) \text{ and }(12) \\ \quad \quad (14) & By \land Cy \implies Dy & \forall-\text{Elimination of }(2) \\ \quad \quad (15) & Dy & \text{Modus Ponens of }(13) \text{ and } (14) \\ \quad \quad (16) & Ryx \land Dy & \land-\text{Introduction of }(7) \text{ and }(15) \\ \quad \quad (17) & \forall \langle y,~ Ryx \land Dy \implies Dx \rangle & \forall-\text{Elimination of }(4) \\ \quad \quad (18) & Ryx \land Dy \implies Dx & \forall-\text{Elimination of }(17) \\ \quad \quad (19) & Dx & \text{Modus Ponens of }(16) \text{ and } (18) \\ \end{array} } \\ \\ \begin{array} {rlr} \quad (20) & \exists \langle y,~ Cy \land Ryx \rangle & \forall-\text{Elimination of }(3) \\ \quad (21) & Dx & \exists-\text{Elimination of }(20) \text{ and } (6) \vdash (19) \\ \end{array} } \\ \\ \begin{array} {rlr} (22) & \forall \langle y,~ Ryx \implies Ay \rangle \implies Dx & \text{Deduction of }(5) \vdash (21) \\ (23) & \forall \langle x,~ \forall \langle y,~ Ryx \implies Ay \rangle \implies Dx \rangle & \forall-\text{Introduction of }(22) \\ \end{array} \end{array}$$

The possible parsing of the original question, $\forall \langle x,~ \forall \langle y,~ (Ryx \implies Ay) \implies Dx \rangle ~\rangle$, is not provable, which can be established with the model:

$$\Omega = \{1,~ 2\}$$ $$R = \{(1,~ 1),~ (1,~ 2),~ (2,~ 1),~ (2,~ 2)\}$$ $$A = \{1\}$$ $$B = \{1\}$$ $$C = \{2\}$$ $$D = \{~\}$$