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

Question

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?

Answer 1

$\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}}$$

Answer 2

You need to assume the conclusion is false and aim for a reductio proof (this is pretty standard if you want to prove a disjunct and can't individually prove one of the disjuncts).

Here's one way of then completing the proof, more or less by brute force (since at every step you do a fairly standard thing).

$A \to (B \lor C)\\ \quad\quad \neg((A \to B) \lor (A \to C))\\ \quad\quad \quad\quad \quad\quad (A \to B)\\ \quad\quad \quad\quad \quad\quad ((A \to B) \lor (A \to C))\\ \quad\quad \quad\quad \quad\quad \bot\\ \quad\quad \neg(A \to B)\\ \quad\quad \quad\quad \quad\quad (A \to C)\\ \quad\quad \quad\quad \quad\quad ((A \to B) \lor (A \to C))\\ \quad\quad \quad\quad \quad\quad \bot\\ \quad\quad \neg(A \to C)\\ \quad\quad\quad\vdots\\ \quad\quad A\\ \quad\quad \neg B\\ \quad\quad \neg C\\ \quad\quad (B \lor C)\\ \quad\quad\quad \vdots\\ \quad\quad \bot\\ \neg\neg((A \to B) \lor (A \to C))\\ ((A \to B) \lor (A \to C))$

The first dots are filled in using standard moves from the two negated conditionals, the second dots by $\lor$-elimination on $B \lor C$.