# Construction of a derivation when proving equivalence of a logical formula.

Given $$A \wedge B \to C \equiv A \to B \to C$$

We want to show that $$\{ A \to B \to C\} \vdash A \wedge B \to C$$ by constructing a derivation using the natural deduction system $\mathcal{N}_{PL}$.

My question: How do i write down such a derivation? So far I just came up with a "prove" by transformation: \begin{align} &A \to (B \to C)\\ &A \to (\neg B \vee C)\\ &\neg A \vee \neg B \vee C\\ &(\neg A \vee \neg B) \vee C\\ &\neg (\neg A \vee \neg B) \to C\\ &A \wedge B \to C \end{align}

First, your expression $A\rightarrow B\rightarrow C$ is not a well formed formula, you need to bracket it somehow and it makes a difference - the material conditional isn't associative.

Now, when they say to prove it using natural deduction, they mean to prove it using only a specific set of rules, namely the rules of natural deduction.

So, do I get it right that I can just assume things, as follows:

1. Assume $A$
2. Then $B \to C$ (1.)
3. Assume $B$
4. Then $C$ (2., 3., Modus ponens)
5. Then $A \wedge B$ ($\wedge$-introduction, 1., 3.)
6. Then $A \wedge B \to C$ (2., 5.)

No, you do not "just assume things".   You start with a premise, them make and discharge assumptions as required to derive the proof.   Since to prove $(A\wedge B)\to C$, from $A\to(B\to C)$, the assumption you need to discharge will be $(A\wedge B)$, therefore that is the assumption you shall need to make.

1. $A\to (B\to C)$ a premise
2. $\quad A\wedge B$ by assumption
3. $\quad A$ by conjunction elimination ($\wedge$E$_1$, 2)
4. $\quad B\to C$ by conditional elimination ($\to$E, 1,3) aka modus ponens
5. $\quad B$ by conjunction elumination ($\wedge$E$_2$, 2)
6. $\quad C$ by conditional elimination ($\to$E, 4,5) aka modus ponens
7. $(A\wedge B)\to C$ by conditional introduction ($\to$I, 2,6)

Where as when starting with the premise $(A\wedge B)\to C$, there you need to discharge the two assumptions $B$, $A$ to prove $A\to(B\to C)$, so

1. $(A\wedge B)\to C$ a premise
2. $\quad A$ by assumption
3. $\qquad B$ by assumption

$~\vdots$ $~~~\qquad \vdots$

? $~~~\qquad C$ by reasons

? $~~~\quad B\to C$ by conditional introduction ($\to$I, 3,?)

? $~~~A\to (B\to C$ by conditional introduction ($\to$I, 2,?)