How to prove the following formula using an indirect proof

Question

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far.

From here I'm stuck (and I'm not even sure if this is correct). My idea is to use negation intro by assuming the opposite and coming up with a contradiction. I assumed $A$ which led to $B \vee C$ and, as you can see, I'm trying or elim but the only way I can think of doing this is to use conditional intro and then or intro but that seems to only work for a single subproof. In other words, I can't use the assumption of $B$ to say $A \to B$. This is called an indirect proof.

Answer 1

I need to prove that the premise $A \to (B \vee C)$ leads to the conclusion $(A \to B) \vee (A \to C)$. Here's what I have so far. ...

A disjunction is usually proven by reduction to absurdity.   Assume its negation and derive a contradiction.   Typically this involves further assuming the negation of one disjunct aiming to derive the other. $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{A\to (B\vee C)}{\fitch{\lnot((A\to B)\lor(A\to C))}{\fitch{\lnot (A\to B)}{\fitch A{~\vdots\\C}\\A\to C\\(A\to B)\vee(A\to C)\\\bot}\\\lnot\lnot(A\to B)\\A\to B\\(A\to B)\vee(A\to C)\\\bot}\\\lnot\lnot((A\to B)\vee(A\to C))\\(A\to B)\lor (A\to C)}$$

Answer 2

Hint: if you assume $A \to (B \lor C)$, $\lnot(A \to B)$ and $A$, then you can conclude $B \lor C$ and $\lnot B$. Can you take it from there?

Answer 3

It is always a very bad sign when someone has started a bunch of subproofs without indicating what happens at the end of the subproof.

A proof should always have a plan or outline, and subproofs provide the skeleton to do so. But again, you need to indicate what you want to do with the subproof, and that involves indicating what you want as the last line of your subproof. You haven't done that for any of the three subproofs you started, which is exactly why you get in trouble, and get see the forest for the trees.

Now, it is clear that with your first subproof you are hoping to do a proof by contradiction. So, start by creating the proper setup for that:

$A \rightarrow (B \lor C)$

$\quad \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$\quad \text{... skip a bunch of lines ...}$

$\quad \bot$

$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$(A \rightarrow B) \lor (A \rightarrow C)$

Ok, now that we have set that up properly, let's go back inside the subproof, and see how we can derive the contradiction from the premise and the assumption.

Now, it is at this point that you assume $A$. Why?

Actually, I think I know why, because I have seen it all too often: you are probably thinking "ooh, it would be nice to have $A$, because then I can combine that with the premise! OK, so let's jist assume $A$"

OK, the problem with this kind of thinking is that you end up assuming something that you want ... which is always a bad ide, as that will often lead to a circular proof. Indeed, suppose you were indeed to combone $A$ with the premise, and get $B \lor C$ ... OK .... now what?! Well, one thing you can do is to then close the subproof and conclude $A \rightarrow (B \lor C)$ .... but note that now you just get the very premise, i.e. You are getting nowhere.

Here is some general advice on subproofs, that goes back to my initial point about having a plan: before starting any subproof, you should already know how you are going to use that subproof, and in particular, what the last line of your subproof should be, and what rule you will apply after the subproof is done.

Ok, let's regroup. There is really no good reason to assume $A$. Ok, but what should you do on line 3? Well, again, if you had $A$, you could combine that with the premise, but rather than assuming $A$, you could try and make $A$ your new goal. And, to prove $A$, one thing you could do is to assume $\neg A$, and show that that leads to a contradiction.

However, there is a much more straightforward thing to do. The assumption $\neg ((A \rightarrow B) \lor (A \rightarrow C))$ is a negation of a disjunction, and you are probably aware of how by DeMorgan that is equivalent to the conjunction of the negated disjuncts, i.e. to $\neg (A \rightarrow B) \land \neg (A \rightarrow C)$. Now, I suspect you don't have DeMorgan as an inference rule in your specific system, but think about it this way: apprently you should be able to derive both $\neg (A \rightarrow B)$ as well as $\neg (A \rightarrow C)$ from the Assumption. Now, both of those statements are negations, and you probably know the best strategy to prove negations: Proof bu Contradiction!

OK, so we have another piece of our plan:

$A \rightarrow (B \lor C)$

$\quad \neg ((A \rightarrow B ) \lor (A \rightarrow C))$

$\quad \quad A \rightarrow B$

$\quad \quad \text{skip a few lines...}$

$\quad \quad \bot$

$\quad \neg (A \rightarrow B)$

$\quad \quad (A \rightarrow C)$

$\quad \quad \text{skip a few lines ...}$

$\quad \quad \bot$

$\quad \neg (A\rightarrow C)$

$\quad \text{few lines ...}$

$\quad \bot$

$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$(A \rightarrow B) \lor (A \rightarrow C)$

OK, see how this is all nicely organized? How you now have an outline, to which you can add details and provide the missing steps at some later point? That is what you are supposed to do! That is how you keep your proof, and your very thinking organized. Indeed, the very point of doing formal logic proofs is to teach you that very skill of careful organization!

Now, I am going to leave those details to you, but leave you with one more hint: what is $\neg (A \rightarrow B)$ equivalent to? .... try and derive that, do the same for $\neg (A \rightarrow C)$, and you're pretty much done! Good luck!

Answer 4

I assume you are using the proof checker associated with the forallx text. There is no rule in this proof checker that allows inference rules for material implication. So it may not be easy to proceed by negating the goal if it contains conditional statements.

The following attempt to complete the proof shows what might happen:

To discharge the assumption $A$ on line 3, I will likely have to use the law of the excluded middle on $A \lor \lnot A$ which would involve another subproof.

An alternate way to proceed is to negate something equivalent to either the premise or the goal to remove the conditional statements. For example note that the premise is equivalent to $\lnot A \lor (B \lor C)$. If I negate that I can rewrite it using the following equivalences:

$$\begin{align} \lnot (\lnot A \lor (B \lor C)) &\equiv \lnot \lnot A \land \lnot (B\lor C)\\ &\equiv A \land \lnot (B\lor C)\\ \end{align}$$

Rather than using the negation of the conclusion, I will use that statement as the assumption and derive a contradiction. Here is the proof:

The contradiction was derived on line 6. Now I have to continue from this point and derive the the goal itself. This detour of negating a statement equivalent to the premise (or goal) may make it easier to derive the goal.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/