0
$\begingroup$

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.

$\endgroup$
1
2
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.