# Hints and/or help needed for axiomatic deduction

Proof: $\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \vdash \forall x (Rxx \rightarrow \neg Ax)$

Axioma schema's that can be used:

1 $(\forall x(\varphi \rightarrow \psi)) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$
2 $\varphi \rightarrow \forall x \varphi$ ($x$ not free in $\varphi$)
3 $\forall x \varphi \rightarrow [t/x]\varphi$ (only if the term $t$ is free for $x$ in $\varphi$)
a $\varphi \rightarrow (\psi \rightarrow \varphi)$
b $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi \rightarrow \psi)\rightarrow (\varphi \rightarrow \chi))$
c $(\neg \varphi \rightarrow \neg \psi) \rightarrow (\psi \rightarrow \varphi)$

And Modus Ponens for deductions.

What I got so far:

$\Sigma = \{\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)\}$

1 $\Sigma \vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)$ assumption
2 $\vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \rightarrow \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ Axiom schema 3
3 $\Sigma \vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ MP, 1, 2
4 $\vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay) \rightarrow (Az \rightarrow Rzz) \rightarrow \neg Az$ Axiom schema 3
5 $\Sigma \vdash (Az \rightarrow Rzz) \rightarrow \neg Az$ MP, 3, 4

And here is where I get stuck. I'm thinking maybe something like:

6 $Az \rightarrow Rzz \vdash Az \rightarrow Rzz$ auxiliary assumption
7 $\Sigma, Az \rightarrow Rzz \vdash \neg Az$ MP, 5, 6
8 $\vdash \neg Az \rightarrow (\neg Rzz \rightarrow \neg Az)$ Axiom schema a
9 $\Sigma, Az \rightarrow Rzz \vdash \neg Rzz \rightarrow \neg Az$ MP, 7, 8

But then I would be stuck with the auxiliary assumption $Az \rightarrow Rzz$, which I still have to use according to the deduction theorem.

I'm looking for some better suggestions!

EDIT -- THE FULL DEDUCTION

$\Sigma = \{\forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)\}$

1 $\Sigma \vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay)$ assumption
2 $\vdash \forall x \forall y ((Ax \rightarrow Rxy) \rightarrow \neg Ay) \rightarrow \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ Axiom schema 3
3 $\Sigma \vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay)$ MP, 1, 2
4 $\vdash \forall y ((Az \rightarrow Rzy) \rightarrow \neg Ay) \rightarrow (Az \rightarrow Rzz) \rightarrow \neg Az$ Axiom schema 3
5 $\Sigma \vdash (Az \rightarrow Rzz) \rightarrow \neg Az$ MP, 3, 4
6 $\vdash Rzz \rightarrow (Az \rightarrow Rzz)$ axiom a
7 $Rzz \vdash Rzz$ assumption
8 $\Sigma, Rzz \vdash Az \rightarrow Rzz$ MP, 6, 7
9 $\Sigma, Rzz \vdash \neg Az$ MP, 5, 9
10 $\Sigma \vdash Rzz \rightarrow \neg Az$ deduction theorem, 9
11 $\Sigma \vdash \forall x (Rxx \rightarrow \neg Ax)$ Universal generalisation

The hardest part is step 6 and 7. At least, I always fall for it. I just cannot fathom coming up with some "random" formula derived from axiom a, and, even worse, taking the antecedent of that axiom a derived formula and use it as an auxiliary assumption (like step 7 did)...

• Basically, $((Az→Rzz)→¬Az) \rightarrow (Rzz→¬Az)$ is a tautology; thus, using it in step 6, you can "detach" $(Rzz→¬Az)$ and conclude with Gen Th. The question is : what kind of propositional theorems are you allowed to use ? If none, we have to prove it "from scratch" ... Commented May 29, 2014 at 11:26
• @MauroALLEGRANZA The propositional theorems you can use are the ones at the top in my post, labeled a through c. Though I don't see any that will fit $((Az \rightarrow Rzz) \rightarrow \neg Az) \rightarrow (Rzz \rightarrow \neg Az)$, so, as you put it, it has to be recreated from scratch. Commented May 29, 2014 at 11:48
• @MauroALLEGRANZA I was reading through it, as we speak (or type). By the way, do you assume (3) from (2)? What I always found strange, is that this axioma a can be used with any formula; apparently even formulas that do not exist in the set of given formulas of a problem... Not that it happens in this case, but still Commented May 29, 2014 at 11:56
• @MauroALLEGRANZA another thing: everything hinges on $((Az \rightarrow Rzz) \rightarrow \neg Az) \rightarrow (Rzz \rightarrow \neg Az)$ that you came up with. That was awesome to come up with that, I don't know how I would've seen this. Commented May 29, 2014 at 12:00
• Regarding the "strange" axiom-a, try to "interpret" it, remembering the truth-functional property of $\rightarrow$. If $\psi$ is true, then a conditional whatever of the "form" $\varphi \rightarrow \psi$ will be true also, because $p \rightarrow q$ is $T$ when $q$ is $T$, independently of the truth-value of $p$. This is the "magic" behind the fact that $ψ→(φ→ψ)$ is a tautology, and thus we can use it as axiom. Commented May 29, 2014 at 12:07

We need :

$(\varphi \rightarrow \psi) \rightarrow \lnot \varphi \vdash (\psi \rightarrow \lnot \varphi)$.

Proof :

(1) $(\varphi \rightarrow \psi) \rightarrow \lnot \varphi$ --- assumed

(2) $\psi \rightarrow (\varphi \rightarrow \psi)$ --- Ax.a

(3) $\psi$ --- assumed

(4) $\varphi \rightarrow \psi$ --- from (2) and (3) by modus ponens

(5) $\lnot \varphi$ --- from (1) and (4) by modus ponens

(6) $\psi \rightarrow \lnot \varphi$ --- from (3) and (5) by Deduction Theorem.

Now you can restart from your :

5 $Σ \vdash (Az→Rzz)→¬Az$

to derive :

6 $Σ \vdash (Rzz→¬Az)$.

• More generally, instead of deriving ((φ→ψ)→¬φ)⊢(ψ→¬φ) one could derive ((φ→ψ)→$\chi$)⊢(ψ→$\chi$). There exists a few three axiom bases for propositional calculus with (((φ→ψ)→$\chi$)→(ψ→$\chi$)). Commented May 29, 2014 at 15:06