# What are the conditions for RAA?

My textbook states that: In this case, however, what about situations where we can get Q ^ ~Q (sorry, unfamiliar with this formatting) without depending on P? For instance, the proof of EFQ:

``````1   (1) P       A
2   (2) ~P      A
3   (3) ~Q      A
1,2 (4) P ^ ~P  1^2
1,2 (5) ~~Q     3,4 RAA
1,2 (6) Q       5 DN
``````

Why isn't it a problem that line 5 does not depend on line 3, when it is the negation of line 3 that we are proving? If we take the above definition of RAA to be true, don't we need 3 to be a dependency of P ^ ~P?

• You have only exchange P and Q... You have derived P ^ ~P from ~Q. Thus, apply RAA rule to get ~~Q. – Mauro ALLEGRANZA May 22 at 17:48

It only seems like a problem if we think the set Γ is consistent, in which case we feel like it's P which "makes" the premises inconsistent, and so must be used in the proof. But if Γ is already inconsistent, then we don't need to use P at all. Think about it in cases:

If Γ is consistent, and Γ, P ⊢ Q ∧ ¬Q, then {Γ, P} is inconsistent, so that Γ ⊢ ¬P

If, on the other hand, Γ is already inconsistent (as in your example proof), then Γ ⊢ ¬P anyways (since inconsistent sets of statements can prove anything).

• Aha that makes sense! Thank you. – user538118 May 22 at 19:09
• Happy it helped :) – Adam Sharpe May 22 at 21:11

Why isn't it a problem that line 5 does not depend on line 3, when it is the negation of line 3 that we are proving?

Because the rule of RAA states that whenever you have Γ, R Ⱶ P ^ ~P, then you may infer that Γ Ⱶ ~R.

Now, as Γ Ⱶ P ^ ~P when Γ is {P, ~P}, therefore we can add any additional premise, such as ~Q, and obtain the required sequent so as to be able to apply Reduction To Absurdity: Γ, ~Q Ⱶ P ^ ~P therefore Γ Ⱶ ~~Q

Here's the full sequent notation for the proof:

``````1     (1)         P Ⱶ P         A
2     (2)        ~P Ⱶ ~P        A
3     (3)        ~Q Ⱶ ~Q        A
1,2   (4)     P, ~P Ⱶ P ^ ~P    1^2
1,2,3 (X) P, ~P, ~Q Ⱶ P ^ ~P    3,4 (skipped this line)
1,2   (5)     P, ~P Ⱶ ~~Q       X RAA (discharges assumption of ~Q)
1,2   (6)     P, ~P Ⱶ Q         5 DN
``````