1
$\begingroup$

I am trying to formulate a proof for:

1. ~Q → (L → F)  
2.  Q → ~A  
3.  F → B  
4.  L           ∴ ~A v B
---------------------------
5.  ~Q       Assume for(CP)
6.   L → F   1,5. MP
7.   L → B   3,4,6. HS
8.   B       4,7. MP
9.  ~A • B   Assume(For RAA)
10. ~A       Simp
11.  A       2,5. MT
12.  A • ~A  Add
13. ~A v B   9-12 RAA, 5-13 CP

Would you put RAA and CP in the same line like this?

$\endgroup$
8
  • 1
    $\begingroup$ And what are you trying to prove, using your CP? CP's are usually employed for deriving a conditional A -> B, by first assuming A (first line of the CP) and then ending up at B (end of the CP). $\endgroup$ Commented Oct 13, 2017 at 3:27
  • 1
    $\begingroup$ I assume ~Q and derive B and then use Reductio ad Absurdum to prove ~A v B $\endgroup$
    – Anon
    Commented Oct 13, 2017 at 3:30
  • $\begingroup$ Right now it looks like you have tried to derive (~Q) [the first line of your CP] → (~A v B) [the last line of your CP]. $\endgroup$ Commented Oct 13, 2017 at 3:33
  • $\begingroup$ I think I understand now. The CP and RAA are not nested in this case. $\endgroup$
    – Anon
    Commented Oct 13, 2017 at 3:33
  • 1
    $\begingroup$ What are you trying to prove using RAA? If you want to prove ~A v B, you should assume ~(~A v B), which, by De Morgan, gives A • ~B. $\endgroup$ Commented Oct 13, 2017 at 3:51

3 Answers 3

1
$\begingroup$
  1. is supposed to be Q -> ~A

In that case, one approach might be to just go for a reductio ad absurbum in the following way:

    1. ~Q → (L → F)  
    2.  Q → ~A  
    3.  F → B  
    4.  L           ∴ ~A v B
    ---------------------------
    5.  ~(~AvB)  Assume for RAA
    6.      A • ~B  5 DeM
    7.      A       6 simp
    8.      ~B      6 simp
    9.      ~F      3,8 MT
    10.     ~Q      2,7 MT
    11.     L → F  1,10 MP
    12.     F       4,11 MP
    13.     ~F • F  9,12 Add 
    14. ~A v B   5-12 RAA

Another pretty fun approach would be to do a conditional proof of $A\to B$ and then use a conditional exchange to obtain $\lnot A \lor B$. It would be a good exercise to try that out yourself

$\endgroup$
0
$\begingroup$

With help from the comments:

1. ~Q → (L → F)  
2.  Q → ~A  
3.  F → B  
4.  L           ∴ ~A v B
---------------------------
5.  ~Q       Assume for(CP)
6.   L → F   1,5. MP
7.   L → B   3,4,6. HS
8.   B       4,7. MP 1-8 CP
9.  ~A v B   Add
$\endgroup$
6
  • 1
    $\begingroup$ If line 11 is by reason of "2, 10 MT" it should contain $\neg Q$ because it is $\{Q\to A, \neg A\}\vdash \neg Q$ by modus tollens (denying the consequent). $\endgroup$ Commented Oct 13, 2017 at 3:46
  • $\begingroup$ i messed up 2. is supposed to be Q -> ~A $\endgroup$
    – Anon
    Commented Oct 13, 2017 at 3:55
  • 2
    $\begingroup$ Okay! No need for Reducto Ad Absurdum (or way to do it). That conditional proof concludes with $\neg Q\to (\neg A\vee B)$. Then you perform another CP (by assuming the contrary $Q$) to likewise conclude $Q\to(\neg A\vee B)$. That allows a proof by cases (aka disjunctive elimination) and you are done.$${Q\to (\neg A\vee B)\\{\neg Q\to (\neg A\vee B)}}\over{\therefore\quad\neg A\vee B}$$ $\endgroup$ Commented Oct 13, 2017 at 4:10
  • 1
    $\begingroup$ I feel like such a dummy. Unfortunately, disjunctive elimination is not in the current chapter of my textbook, however, looking at it all I need to do is assume A or assume ~B and the proof falls off the page! $\endgroup$
    – Anon
    Commented Oct 13, 2017 at 4:20
  • $\begingroup$ You can use Excluded Middle: $Q \lor \lnot Q$ and apply $\lor$-elim to it. The branch with $Q$ is straightforward: $\lnot A$ from 2 and then $\lnot A \lor B$ by $\lor$-intro, $\endgroup$ Commented Oct 13, 2017 at 7:51
0
$\begingroup$

i messed up 2. is supposed to be Q -> ~A

Then there you do not require RAA. Use a proof by cases.

$\begin{array}{r:ll}1 & \lnot Q \to (L \to F)\\ 2& Q \to \neg A \\ 3 & F \to B \\ 4 & L \\\hdashline 5 & \quad \neg Q &\text{Assume} \\ 6 & \quad L\to F & 1,5, \to\text{Elim, aka modus ponens} \\ 7 & \quad F & 4,6 , \to\text{Elim}\\ 8 & \quad B & 4,7 , \to\text{Elim}\\ 9 & \quad \neg A\vee B & 8, \vee \text{Intro, aka Addition}\\\hline 10 & \neg Q\to (\neg A\vee B) & 5,9, \to\text{Intro, aka Deduction Theorem}\\ \hdashline 11 & \quad Q & \text{Assume}\\ 12 & \quad \neg A & 2, 11, \to\text{Elim}\\ 13 & \quad \neg A\vee B & 12, \vee\text{Intro}\\ \hline 14 & Q\to (\neg A\vee B) & 11,13,\to\text{Intro}\\ 15 & Q\vee\neg Q & \text{Law of Excluded Middle}\\ 16 & \neg A\vee B & 10,14,15 \vee\text{Elim, aka proof by cases} \end{array}$

PS: Constructive Dilemna would have also sufficed.   $5,8$ deduces $\neg Q\to B$ and with $2$ we have $\{Q\to\neg A, \neg Q\to B\}\vdash \neg A\vee B$


Update: Of course, you may use RAA. Assume the negation and derive a contradiction.   This may be nested: further assume Q, derive a contradiction, thus deducing $\neg Q$ from which a contradiction may also be derived...

$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~\neg Q \to (L \to F)\\~~2.~Q \to \neg A\\~~3.~F \to B\\~~4.~L}{\fitch{~~5.~\neg(\neg A\vee B)}{\fitch{~~6.~Q}{~~7.~\neg A\hspace{10ex}\to\mathsf E, 6,2\\~~8.~\neg A\vee B\hspace{6ex}\vee\mathsf I, 7\\~~9.~\bot\hspace{12ex}\neg\,\mathsf E,5,8}\\10.~\neg Q\hspace{14ex}\neg\,\mathsf I, 6{-}9\\11.~L\to F\hspace{10ex}\to\mathsf E, 10,1\\12.~F\hspace{15ex}\to\mathsf E, 4,11\\13.~B\hspace{15ex}\to\mathsf E, 3, 12\\14.~\neg A\vee B\hspace{10ex}\vee\mathsf I,13\\15.~\bot\hspace{16ex}\neg\,\mathsf E, 5,14}\\16.\neg\neg(\neg A\vee B)\hspace{10ex}\neg\,\mathsf I, 5{-}15\\17.~\neg A\vee B\hspace{14ex}\neg\neg\,\mathsf E,16}$

$\endgroup$

You must log in to answer this question.

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