# Provide a derivation from backwards on?

Suppose you have to provide a derivation by natural deduction, e.g.

$((A \rightarrow B) \rightarrow A) \rightarrow A$

Is it a good advice to start from backwards on in general? I mean doing the derivation from bottom to top. The required premises or hypothesis should arise by itself.

• – brandstifter May 14 '18 at 17:01

In general, proof crafting is a dark art. There is no simple universal strategy which in all cases leads to a proof, in the shortest way, with the least effort. One usually relies on instinct and experience (doing several exercises helps greatly).

Trying to reconstruct the derivation bottom-up is often a good strategy. However, note that in natural deduction (unlike some other systems) going bottom-up one needs to cope with infinitely many possibilities.

For instance, if I have to prove $A$, I could try to deduce it through modus ponens / implication elimination:

$$\dfrac{\dfrac{\vdots}{B\rightarrow A} \qquad \dfrac{\vdots}{B}}{A}$$

However, formula $B$ above could be anything! I have to chose among infinitely many formulas, which is not easy.

Worse, in some cases it is needed to exploit some rule like double negation elimination

$$\dfrac{\lnot\lnot A}{A}$$

It is not obvious when this is needed. For instance, I know that using this rule (or something equivalent like the law of excluded middle) is needed to prove $((A \to B)\to A)\to A$, but I can see this only because this is a very famous logical formula (called Peirce's Law).

At the end of the day, one can try a few heuristics, but should expect to have to backtrack a few times. In general the problem is very hard, but fortunately the exercises which one finds in books / exams usually are solvable with some intuition and little backtracking.

• can you refer to some proofs in books? – brandstifter May 14 '18 at 17:09
• @brandstifter I'm not aware of any books doing significant examples of derivations, I'm sorry. – chi May 14 '18 at 17:57