4

My textbook states that: enter image description here

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 '19 at 17:48
7

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

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

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
| improve this answer | |

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.