Proving $A \to (B \vee C) \therefore (A \to B) \vee (A \to C)$

logicnatural-deduction

In P.D. Magnus. forallX: an Introduction to Formal Logic (pp. 154), appears this exercise:

$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\fitch{A \to (B \vee C)}{
\fitch{A}{
B \vee C \\
\fitch{B}{
\fitch{\neg(A \to B)}{
\fitch{A}{
B
} \\
A \to B \\
\bot
} \\
A \to B \\
(A \to B) \vee (A \to C)
}\\
\fitch{C}{
\fitch{\neg(A \to C)}{
\fitch{A}{
C
} \\
A \to C \\
\bot
} \\
A \to C \\
(A \to B) \vee (A \to C)
}\\
(A \to B) \vee (A \to C)
}
}
$

In this stage, I reached the conclusion but I am inside a sub-proof. Is there a way to successfully prove this argument?

Best Answer

$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}$ Remark: Your subproof is somewhat convoluted. Compare: $$\fitch B{\fitch{\neg (A\to B)}{\fitch AB\\A\to B\\\bot}\\\neg\neg(A\to B)\\A\to B\\(A\to B)\vee(A\to C)}\qquad\raise{7.25ex}{\fitch B{\fitch AB\\A\to B\\(A\to B)\vee(A\to C)}}$$

There are two ways to derive a disjunction.

  1. constructively derive one of the disjuncts, or
  2. use an indirrect proof (reduce the negation to absurdity).

You are having trouble doing (1), therefore you should attempt an indirect proof.

Assume $\neg((A\to B)\vee(A\to C))$ and place your proof inside this context.

$$\fitch{~~1.~A\to(B\vee C)}{\fitch{~~2.~\neg((A\to B)\vee(A\to C))}{\fitch{~~3.~A}{~~4.~B\vee C\hspace{20ex}\textsf{Conj.Elim 3,1}\\\fitch{~~5.~B}{\fitch{~~6.~A}{~~7.~B\hspace{20ex}\textsf{Reiteration 5}}\\~~8.~A\to B\hspace{17ex}\textsf{Conj.Intro. 6-7}\\~~9.~(A\to B)\vee (A\to C)\hspace{4ex}\textsf{Disj.Intro. 8}\\10.~\bot\hspace{22.5ex}\textsf{Neg.Elim. 9,2}\\11.~C\hspace{22.5ex}\textsf{Explosion 10}}\\\fitch {12.~C}{}\\13.~C\hspace{25ex}\textsf{Disj.Elim. 4,5-11,12-12}}\\14.~A\to C\hspace{22ex}\textsf{Conj.Intro 3-13}\\15.~(A\to B)\vee(A\to C)\hspace{9ex}\textsf{Disj.Intro 14}\\16.~\bot\hspace{27.5ex}\textsf{Neg.Elim. 2,15}}\\17.~\neg\neg((A\to B)\vee(A\to C))\hspace{6.5ex}\textsf{Neg.Intro. 2-16}\\18.~(A\to B)\vee(A\to C)\hspace{11.5ex}\textsf{Double Neg.Elim. 17}}$$

Related Question