Prove using inference rules

Question

I'm having trouble proving this using inference rules...

$(A\to (B\to C)\to (B\to (\sim C\to\, \sim A ))$

Perhaps, I should start with $A\to (\sim B\lor C)$??

Help!

Answer 1

This sort of derivation should really cause you no problem if you think strategically.

Think: what's the default strategy for proving a conditional in a natural deduction system? Assume the antecedent and try to derive the consequent; then you can apply conditional proof. So let's go for this. So you should now be aiming to fill in the dots in the following

$\quad\quad|\quad (A \to (B \to C)) \quad\quad\quad\quad\quad\quad\quad\quad \text{Assumption, for the sake of argument} \\ \quad\quad|\quad \ldots \\ \quad\quad|\quad (B \to (\neg C \to \neg A)) \\ (A \to (B \to C)) \to (B \to (\neg C \to \neg A)) \quad \quad\ \ \ \text{CP: Discharging the initial assumption} $

Now look at the new target you want to prove. It is another conditional! So we use the same strategy, assume the antecedent and aim for the consequent so we can apply CP. So now the proof outline will look like this:

$\quad\quad|\quad (A \to (B \to C)) \\ \quad\quad|\quad\quad | \quad B \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad \text{A further assumption, for the sake of argument}\\ \quad\quad|\quad\quad |\quad \ldots \\ \quad\quad|\quad\quad | \quad (\neg C \to \neg A)\\ \\ \quad\quad|\quad (B \to (\neg C \to \neg A)) \quad \quad\quad\quad\quad\ \ \ \text{CP: Discharging the second assumption} \\ (A \to (B \to C)) \to (B \to (\neg C \to \neg A))$

And no, low and behold, your new target to prove is another conditional! You know what to do ... You want to complete the following :

$\quad\quad|\quad (A \to (B \to C)) \\ \quad\quad|\quad\quad | \quad B \\ \quad\quad|\quad\quad | \quad \quad|\quad \neg C \\ \quad\quad|\quad\quad|\quad\quad |\quad \ldots \\ \quad\quad|\quad\quad | \quad \quad|\quad \neg A \\ \quad\quad|\quad\quad | \quad (\neg C \to \neg A)\\ \\ \quad\quad|\quad (B \to (\neg C \to \neg A)) \\ (A \to (B \to C)) \to (B \to (\neg C \to \neg A))$

OK your new target is $\neg A$, using the first three assumptions. Can you see how to get that? If in doubt, try proving a negation using reductio, so the proof will go

$\quad\quad|\quad (A \to (B \to C)) \\ \quad\quad|\quad\quad | \quad B \\ \quad\quad|\quad\quad | \quad \quad|\quad \neg C \\ \quad\quad|\quad\quad|\quad\quad | \quad \quad|\quad A \\ \quad\quad|\quad\quad|\quad\quad|\quad\quad |\quad \ldots \\ \quad\quad|\quad\quad|\quad\quad|\quad\quad |\quad \mathrm{Contradiction} \\ \quad\quad|\quad\quad | \quad \quad|\quad \neg A \quad\quad\quad\quad\quad\quad\text{Reductio: discharging the assumption } A\\ \quad\quad|\quad\quad | \quad (\neg C \to \neg A)\\ \\ \quad\quad|\quad (B \to (\neg C \to \neg A)) \\ (A \to (B \to C)) \to (B \to (\neg C \to \neg A))$

And now you can fill in the dots (use our latest assumption with the initial one, apply modus ponens, etc.). The proof has pretty much written itself!

Two morals: (1) think strategically and this kind of text-book natural deduction example will usually fall out very easily, with a bit of patience!

(2) Using one of the standard ways of clearly graphically representing the structure of a natural deduction proof is pretty essential to keep tabs on what is going on (so you can see which temporary assumptions are in play at which stage and when they get discharged). [Note: I've used a Fitch-style display both because it is easier to do here on math.se and because it is particularly clear. But you should be able to convert this to a Gentzen-style tree display easily enough.]