Show there's no RAA-free derivation of $(P_1\to P_2)\lor (P_2\to P_1)$

Question

Show there's no RAA-free derivation of $(P_1\to P_2)\lor (P_2\to P_1)$. (Hint: Look for a normal such derivation.)

Solution:

Here are the theorems we have learnt from the normal deduction chapter.

---

Theorem 1 (Glivenkos theorem): Every derivation can be transformed so that in the end it becomes a derivation in which RAA does not occur except possible at the last step, and in which all undischarged assumptions occurred (as undischarged assumptions) in the original derivation.

Theorem 2. If $Γ\to ⊥$, then there exists an RAA-free derivation from Γ to ⊥.

Theorem 3 (weak normalization): Every derivation can be transformed in such a way that a normal derivation is reached, in which all undischarged assumptions existed already (as undischarged assumptions) in the original derivation. If the original derivation was RAA-free then the resulting derivation consists only on the rules that were used in the original one.

Theorem 4: If a normal derivation ends in an elimination rule, then the main premise is a subformula in some undischarged assumption.

Theorem 5 (subformula property): In every normal derivation without RAA, every formula is a subformula of either the conclusion or one of the undischarged assumptions of the derivation.

Theorem 6: Assume that $Γ\vdash ϕ$.

1. If $ϕ$ is a ∧-formula, then there is a normal derivation from $Γ$ to $ϕ$ which ends with $∧I$.

2. If $ϕ$ is a →-formula, then there is a normal derivation from $Γ$ to $ϕ$ which ends with →I.

---

So let's assume there's a normal RAA-free derivation. At this point I would say that the last theorem won't help me. Neither won't, I guess, the first or second theorem. I have already used the third Theorem so the only theorems which are left to use is Theorem 4 and Theorem 5?

A little side note: A friend to me told me, when I have an or-formula, then I NEED to end with an $\lor$-introduction. And if I then have an implication rule then I NEED to use an $\to$-introduction.

It would look like this $\frac{\frac{P_2}{P_1\to P_2}\to I}{(P_1\to > P_2)\lor (P_2\to P_1)}\lor I.$

But I have not seen, or at least I think so, any theorem which states I have to end with an or introduction rule if my conclusion is an or-formula. Neither do I know why the only possibility (in a general case) is to use an implication introduction as my second last rule. I don't know if he thinks that theorem 6 says that if you have an implication formula then you have to use implication introduction. Perhaps he has misread the theorem. Because it really says that if $\phi$ is an implication formula then it has to end with an implication introduction (also my $\phi$ is an or-formula).

So perhaps I can use the subformula property and show it can't hold? I am a little rusty when it comes to this kind of exercises. I know my goal but sometimes it's pretty hard for me to end up there. I think it would be pretty simple if my tree in the yellow box were correct, but I don't think it is correct. Any help would be appreciated. Perhaps, if it is possible, some help how to think if I try to solve other similar problems. Where should i start? How should I think? Perhaps I only have to solve many problems? Thank you :)

Answer 1

Hint

See :

• Dirk van Dalen, Logic and Structure (5th ed - 2013), page 204 for intuitionistic logic :

Theorem 7.3.11 Let $Γ \vdash ϕ ∨ ψ$, where $Γ$ does not contain $∨$ in strictly positive subformulas, then $Γ \vdash ϕ$ or $Γ \vdash ψ$

Thus, if $(P \to Q) \lor (Q \to P)$ is derivable without RAA, the derivation would hold intuitionistically.

Applying the above Theorem with $\Gamma = \emptyset$, we would conclude that :

either $\vdash ( P \to Q)$ or $\vdash (Q \to P)$

but neither are intuitionistically valid.