1 Complete the proof of soundness of propositional logic (given in van Dalen, Lemma 1.5.1) with the case of !E. 2 Prove the soundness of the _ rules (_I and _E). 3 Do we have j= (p ! q) _ (q ! r)? 4 Do we have (q ! (p _ (q ! p))) _ :(p ! q) j= p? 5 Assuming the soundness and completeness of natural deduction for propositional logic, suppose that you need to show that φ is not a semantic consequence of φ1; φ2; :::; φn, but that you are only allowed to base your argument on the use of natural deduction rules. Which judgement would you need to prove in order to guarantee that φ1; φ2; :::; φn 6j= φ? Do you need completeness and soundness for this to work out?
6 Consider the following axiom based system, called Hilbert system: (φ ! ( ! φ)) ((φ ! ( ! σ)) ! ((φ ! ) ! (φ ! σ))) ((:φ ! : ) ! ((:φ ! ) ! φ)) Combined with the Modus Ponens inference rule, which corresponds to the elimination rule of the implication connective. Prove according to this system the judgement ‘ φ ! φ. 7 Consider classical logic given in the handout \Natural deduction in sequent form" in Figure 5. Prove the following judgements: ‘ φ _ :φ (This is called Law of Excluded Middle). ((φ ! ) ! φ) ! φ (This is called Peirce’s Law) 8 Prove the following judgements: A ! B ! A (A ! B ! C) ! (A ! B) ! (A ! C) (A ^ B ! C) ! (A ! B ! C) (A ! B ! C) ! (A ^ B ! C) Annotate each proof with lambda-terms.
