3
$\begingroup$

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)...

$\endgroup$
  • 1
    $\begingroup$ 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" ... $\endgroup$ – Mauro ALLEGRANZA May 29 '14 at 11:26
  • $\begingroup$ @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. $\endgroup$ – Garth Marenghi May 29 '14 at 11:48
  • $\begingroup$ @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 $\endgroup$ – Garth Marenghi May 29 '14 at 11:56
  • $\begingroup$ @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. $\endgroup$ – Garth Marenghi May 29 '14 at 12:00
  • $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA May 29 '14 at 12:07
2
$\begingroup$

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)$.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.