Constructing Proof Trees for Natural Deduction

Question

I'm in the process of learning the process of writing so-called proof trees for $\textit{Natural Deduction}$. One question that I still grapple with is the actual process According to Van Dalen ($\textit{Logic and Structure}$ p. 35):

"After making a number of derivations one gets the practical conviction that one should first take propositions apart from the bottom upwards, and then construct the required propositions by putting together the parts in a suitable way".

Am I right to interpret this as saying that when one seek to construct a proof, one works the opposite way compared to how one later reads it. For example, if I would want to prove:

$$\neg(P_{1} \to P_{2}) \leftrightarrow(P_{1} \lor \neg P_{2})$$ then for the $\to$ part , I would start with $(P_{1} \lor \neg P_{2})$ and notice that a suitable rule before the conclusion would be the inclusion rule, and work my way upwards.

Answer 1

Yes. Think strategically all the time, in terms of the current target you want to prove. So how could you prove [to take your actually given example]

$\neg(P \to Q) \to (P \lor \neg Q)$

in van Dalen's Gentzen-style system? You'll surely need a proof of the form

$\quad\neg(P \to Q)$

$\quad\quad\ldots$

$\quad(P \lor \neg Q)$

$\_\_\_\_\_\_\_\_\_\_\_\_$

$\neg(P \to Q) \to (P \lor \neg Q)$

So now, moving up a step, you new target is to get to $(P \lor \neg Q)$. And the chances are that for that, you'll need a step of $\lor$I -- in fact (pretty obviously) the proof to try is

$\quad\neg(P \to Q)$

$\quad\quad\ldots$

$\quad\quad \neg Q$

$\quad(P \lor \neg Q)$

$\_\_\_\_\_\_\_\_\_\_\_\_$

$\neg(P \to Q) \to (P \lor \neg Q)$

Your new target is $\neg Q$. And so it goes ...

[Are you sure about the example though? For the converse implication, you'll need a conjunction not a disjunction!]