CIS 527 Homework 4

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.