Homework (I)

Problem For each of the propositions below, first draw the parsing tree, and then construct a natural deduction proof.

1. or_distributes_over_and: $P\vee (Q \wedge R) \Rightarrow (P\vee Q)\wedge (P\vee R)$
2. application_tautology: $P \To (P \To Q) \To Q$
3. disjuntion_to_implication: $\neg P \lor Q \To P \To Q$
4. negation_implication_negation_of_negation: $(\neg P \To P) \To \neg \neg P$

Tips

1. Be sure to name each rule that you use in your natural deduction proofs with a small annotation on the right side of inference rule lines as we did in the lectures.
2. or_distributes_over_and, application_tautology, etc. are names; you have to construct a proof for the propositional formulae written in front of them.
3. Examples relevant to the homework problems: Be sure to go over all the examples in the summary slides.
4. One thing that makes natural deduction confusing is that hypotheses can be eliminated (aka canceled) according to the elimination rules of inference. To understand this better let’s have a look at the slide “conjunction distributes over disjunction” in the summary slides: We have an implication as the outer-most (the top-most in the parsing tree) connective, and we want to construct a proof of that implication which has a premise, namely $P \land (Q \lor R)$ and a conclusion, namely $(P \land Q) \lor (P \land R)$. Note that the outer-most connective of the premise is conjunction. Since we want to go from the premise to conclusion, we want to use the information about its truth to infer the conclusion, that is how can we use/eliminate the assumption $P \land (Q \lor R)$ and out of it construct a proof of conclusion $(P \land Q) \lor (P \land R)$. The elimination rules of conjunction show the way for us.
5. The annotation numbers “1, 2, 3, …” on the right side of the horizontal inference lines are for introducing and eliminating hypothesis according to the applied rules of inference. For instance in the above-mentioned example from the slides we see “1” above $P \land (Q \lor R)$ which appears according to the introduction rule of implication $P \land (Q \lor R) \To (P \land Q) \lor (P \land R)$. Furthermore, the hypothesis $P \land (Q \lor R)$ is cancelled at the very last line again according to the introduction rule of implication, and that is why we put number “1” as annotation to signal that we are cancelling hypothesis “1”. What about annotation “2”? How did that appear? In the proof tree we inferred $(Q \lor R)$ from $P \land (Q \lor R)$. We use the elimination rule of disjunction to prove $(P \land Q) \lor (P \land R)$ under assumption $Q$ and under assumption $R$. Therefore, we need to track the assumptions $Q$ and $R$ we just introduced according to the single rule of disjunction elimination, and this is what we use the same number “2” for both $Q$ and $R$.
6. For Q3, when we want to prove $\neg P \lor Q \To P \To Q$ the first thing to notice is that the first implication is the top-most connective in the corresponding parsing tree and that is our first goal. But, how do we prove an implication? The only way we know is to use the introduction rule for implication. Therefore, we assume $\neg P \lor Q$ and from that assumption we want to derive $P \To Q$. So, we have to construct a derivation of the sequent $\neg P \lor Q \vdash P \To Q$ But how do we use a disjunctive assumption? Well, the elimination rule of disjunction tells us we have to prove $P \To Q$ under the assumptions $\neg P$ and $Q$ separately. So, our goal reduces to the sub-goals of construction of derivations of sequents $\neg P \vdash P \To Q \quad \text{and} \quad Q \vdash P \To Q$ In both cases, we are trying to prove an implication, and so we use the implication introduction rule again …