Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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.
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.
