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?

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

2 Answers 2

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

2
  • Aha that makes sense! Thank you.
    – user538118
    May 22, 2019 at 19:09
  • Happy it helped :) May 22, 2019 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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .