# Fill out this derivation..

I'm having immense trouble trying to fill out the blanks in this proof.

$\newcommand{\tofrom}{\leftrightarrow} \boxed{\begin{array}{l|l:l} 1. & (A\tofrom \neg B) & \text{Premise} \\ 2. & (C\to (\neg\neg D \wedge E)) & \text{Premise} \\ 3. & \neg B & \text{Premise} \\\hline 4. & & \text{Assumption} \\ 5. & & \tofrom\text{ Elimination }1,3 \\ 6. & & \to\text{ Elimination }2, 4 \\ 7. & & \wedge\text{ Elimination }6 \\ \hline 8. & & \text{Assumption} \\ 9. & & \neg \text{ Introduction } 7, 8 \\ \hline 10. & & \neg\text{ Elimination } 9 \\ 11. & & \vee \text{ Introduction } 10 \\ 12. & & \wedge \text { Introduction } 11, 5 \\ \hline 13. & C \to ((D\vee H)\wedge A) & \to\text{ Introduction } 12 \end{array} }$

Click the blue text. It is an image.

• Click the blue text.. it's a link to the image. @Dylan – sefor Oct 28 '15 at 19:31
• MathJaxed Text is preferred over offsite images. @sefor – Graham Kemp Oct 29 '15 at 2:34
• @Andres Caicedo awesome table, sir :). – YoTengoUnLCD Oct 29 '15 at 17:44

Assume [a] : $C$

From 1) and 3) derive : $A$

From 2) and $C$ derive : $\lnot \lnot D \land E$

From $\lnot \lnot D \land E$ derive $\lnot \lnot D$ by $\land$-elim

Assume [b] : $\lnot D$

Derive a contradiction : $\bot$

Derive : $D$ from the contradiction, discharging assumption [b]

Derive : $D \lor H$ by $\lor$-intro

Derive : $(D \lor H) \land A$ by $\land$-intro

Conclude with : $C \to [(D \lor H) \land A]$ by $\to$-intro, discharging [a].

Work backwards.

For instance, step 13 is $\to$ introduction. This will be discharging the assumption of the indented block. We have $C\to\ldots$ in line 13, so $C$ is the assumption of line 4, and the consequence of the implication is line 12.

This in turn allows you to suspect that $D\vee H$ and $A$ were $\wedge$ introduced from line 11 or 5. But which was which. Well, 11 is a $\vee$ introduction and only one term has a $\vee$. Also line 5 is a $\tofrom$ elimination from lines 1 and 3, and you should be able to see which term that will be.

$\newcommand{\tofrom}{\mathop{\leftrightarrow}} \boxed{\begin{array}{l|l:l} 1. & (A\tofrom \neg B) & \text{Premise} \\ 2. & (C\to (\neg\neg D \wedge E)) & \text{Premise} \\ 3. & \neg B & \text{Premise} \\\hline \quad 4. & \color{red}{C} & \text{Assumption} \\ \quad 5. & \color{blue}{A} & \tofrom\text{ Elimination }1,3 \\ \quad 6. & & \to\text{ Elimination }2, 4 \\ \quad 7. & & \wedge\text{ Elimination }6 \\ \hline \qquad 8. & & \text{Assumption} \\ \qquad 9. & & \neg \text{ Introduction } 7, 8 \\ \hline \quad 10. & & \neg\text{ Elimination } 9 \\ \quad 11. & \color{blue}{D\vee H} & \vee \text{ Introduction } 10 \\ \quad 12. & \color{red}{(D\vee H)\wedge A} & \wedge \text { Introduction } 11, 5 \\ \hline 13. & C \to ((D\vee H)\wedge A) & \to\text{ Introduction } 12 \end{array} }$

And so forth.

When you make an assumption, you're going to want to discharge it. You'll probably assume something to do one of the following:

1. Derive a conditional. In this case you introduce an assumption and then discharge it into a formula.
2. Deduce a negation. In this case you assume the negated formula without the negation.
3. Get to a positive formula, or in other words a formula that does not have a negation symbol as it's principal connective. In this case, you'll assume the negation of the formula that you want to find.

Now, you're trying to deduce a conditional. So, you'll probably want to start by assuming the antecedent. Thus, what would step 4 make sense as?

For the steps that aren't assumptions, take a look at the rules of inference and make substitutions for all instances of a particular meta-variable throughout the rule *according to what gets suggested on the right hand side. And make sure to use fully parenthesized formulas when substituting (or switch to Polish/Reverse Polish notation).

For example, let's say I wrote the following outline trying to prove $\vdash$ ((P $\land$ Q) $\rightarrow$ (Q $\land$ P)):

1.        assumption
2.        1 conjunction elimination-left
3.        1 conjunction elimination-right
4.        3, 2 conjunction introduction
5.        1-4 conditional introduction


By the first part above, 1. follows as (P $\land$ Q). The conjunction elimination-left rule says:

($\alpha$ $\land$ $\beta$) $\vdash$ $\alpha$

Thus, substituting P for $\alpha$ and Q for $\beta$ in the conjunction elimination left rule we have:

(P $\land$ Q) $\vdash$ P

Thus, step 2. is P.

The conjunction-elimination right rule says

($\alpha$ $\land$ $\beta$) $\vdash$ $\beta$

By a similar argument to the above, step 3 is Q.

The conjunction introduction rule says $\alpha$, $\beta$ $\vdash$ ($\alpha$ $\land$ $\beta$)

Uniformly substituting Q for $\alpha$ and P for $\beta$ thus we have

Q, P $\vdash$ (Q $\land$ P).

Thus, step 4. comes as (Q $\land$ P).

Finally, we discharge the assumption and deduce $\vdash$ ((P $\land$ Q) $\rightarrow$ (Q $\land$ P))

Now your system doesn't have a conjunction elimination left rule and a conjunction elimination right rule. However, the conjunction rule that you have probably comes as equivalent to having both rules. Similarly, some other rules might get broken down this way.

Hopeful with that in mind you'll have the ability to solve similar sorts of problems in the future.