Logic and Axiomatic Semantics
Homework #3,
Part I, Formal logic: Provide formal proofs, as illustrated in the class notes, for the following theorems:
1. ((P ⇒ R)∧(Q ⇒ S)) ⇒ ((P ∧Q) ⇒ (R∧S)) 2. (P ⇒ (Q ⇒ R)) ⇒ (Q ⇒ (P ⇒ R)) 3. (P ⇒ (P ⇒ Q)) ⇒ (P ⇒ Q) 4. ((P ⇒ Q) ⇒ Q) ⇒ ((Q ⇒ P) ⇒ P) 5. (P ⇒ Q)∨(Q ⇒ P) 6. ((P ⇒ R)∨(Q ⇒ R)) ⇒ (P ∧Q ⇒ R) 7. (P ∧Q ⇒ R) ⇒ ((P ⇒ R)∨(Q ⇒ R))
Part II, Axiomatic Semantics: Provide formal proofs of the following triples.
8. {x 5} x = 2 * x {x 8} 9. {y 0} if x y then y = x + y {y 0}
Part III, Concurrency:
10. Provide a formal proof of the following. Show both the annotated code, and proofs of all necessary triples. {x = 2∧y = 3} co x = y; // y = 4; oc {x = 3∨x = 4}
1
I provide here an example using the natural deduction package for L ATEX. Further examples are in the lectures. Prove: (P ⇒ Q) ⇒ ((P ∧R) ⇒ (Q∧R))
1. P ⇒ Q assumption for conditional proof 2. P ∧R assumption for conditional proof 3. P 2, simplification
4. R 2, simplification
5. Q 1, 3, modus ponens 6. Q∧R 4, 5, conjunction
7. (P ∧R) ⇒ (Q∧R) conditional proof
8. (P ⇒ Q) ⇒ ((P ∧R) ⇒ (Q∧R)) conditional proof
