Prove in axiomatic system S

Question

The question is to prove this in the axiomatic system S:

$$(\forall x)(\forall y)((A_x \rightarrow R_{xy}) \rightarrow \neg A_y) \vdash (\forall x)(R_{xx} \rightarrow \neg A_x) $$

The problem is, I don't have any idea how to begin. The axioms about quantors can be used, in addition to the following axioms, but for this example I don't know with which axiom to start first:

1. $A\rightarrow (B \rightarrow A)$

2. $(A\rightarrow (B\rightarrow C)) \rightarrow ((A\rightarrow B)\rightarrow (A\rightarrow C))$

3. $(\lnot A\rightarrow \lnot B)\rightarrow (B\rightarrow A)$

Answer 1

Hint

1) $(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay)$ --- premise

2) $(Ax → Rxx) → ¬Ax$ --- from Ax: $\forall x \alpha \to \alpha[t/x]$ and 1) by modus ponens twice

3) $Rxx$ --- assumed [a]

4) $Rxx \to (Ax \to Rxx)$ --- Ax.1

5) $Ax \to Rxx$ --- from 3) and 4) by mp

6) $¬Ax$ --- from 5) and 2) by mp

7) $Rxx \to ¬Ax$ --- from 3) and 6) by Deduction Th

8) $\forall x \ (Rxx \to ¬Ax)$ --- from 7) by Generalization.

---

To be more "formal", we have to omit 1) and 3), and step 2) is:

2') $(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay), Rxx \vdash (Ax → Rxx) → ¬Ax$

while step 4) is:

4') $\vdash Rxx \to (Ax \to Rxx)$

and so on :

5') $(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay), Rxx \vdash Ax \to Rxx$

6') $(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay), Rxx \vdash ¬Ax$

from which, by Deduction Th : if $\Gamma, \alpha \vdash \beta$, then $\Gamma \vdash \alpha \to \beta$, where $\Gamma = \{ \ (∀x)(∀y) \ ((Ax → Rxy) → ¬Ay) \ \}$ :

7') $(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay) \vdash Rxx \to ¬Ax$

and finally:

$(∀x)(∀y) \ ((Ax → Rxy) → ¬Ay) \vdash (∀x) \ (Rxx \to ¬Ax)$.

Answer 2

Don't know which syntax/basic rules you need to use, but generally it'll be something like this:

$$(\forall x)(\forall y)((A_x \rightarrow R_{xy}) \rightarrow \neg A_y)$$ $$(\forall x)((A_x \rightarrow R_{xx}) \rightarrow \neg A_x)$$ ($\forall$ elimination) $$(\forall x)(\neg (A_x \rightarrow R_{xx}) \vee \neg A_x)$$ (definition of $\rightarrow$ elimination, for some systems; if you don't have it, you should prove it from what you're given) $$(\forall x)(\neg (\neg A_x \vee R_{xx}) \vee \neg A_x)$$ ($\rightarrow$ elimination) $$(\forall x)((A_x \wedge \neg R_{xx}) \vee \neg A_x)$$ (de morgan's) $$(\forall x)(\neg R_{xx} \vee \neg A_x)$$ ($\wedge$ elimination) $$(\forall x)(R_{xx} \rightarrow \neg A_x)$$ ($\rightarrow$ introduction)