5

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

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

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.