CIS301 Monday, March 10 NAME___sample solution________ Write a proof of this sequent. Consciously apply (some of) the tactics for ^i, ve, and ->i, and you will find the proof easily. p -> r, q -> s |- (p v q) -> (r v s) Tactic 1: Since -> is the main connective in the goal, apply the ->i tactic: assume (p v q) in a box and try to prove (r v s): 1. p -> r premise 2. q -> s premise +----------------------- | 3. p v q assumption | | | m. r v s +----------------------- m+1. (p v q) -> (r v s) ->i 3-m Tactic 2: Since v appears in a fact, apply the ve tactic: assume p in one box, q in another box, and try to prove (r v s) in both: 1. p -> r premise 2. q -> s premise +----------------------- | 3. p v q assumption | +---------------------------- | | 4. p assumption | | | | n. r v s | +---------------------------- | +---------------------------- | | n+1. q assumption | | | | m-1. r v s | +------------------------------ | m. r v s ve 3, 4-n, n+1-m-1 +----------------------- m+1. (p v q) -> (r v s) ->i 3-m Now, fill in the details: 1. p -> r premise 2. q -> s premise +----------------------- | 3. p v q assumption | +---------------------------- | | 4. p assumption | | 5. r ->e 1,4 | | 6. r v s vi1 5 | +---------------------------- | +---------------------------- | | 7. q assumption | | 8. s ->e 2,7 | | 9. r v s vi2 8 | +------------------------------ | 10. r v s ve 3, 4-6, 7-9 +----------------------- 11. (p v q) -> (r v s) ->i 3-10 The tactics we used are listed in Chapter 5's Summary Section, 5.10. The "computer code" in this proof is a function that takes as an argument a "variant value" (tagged pair/struct) and applies an if-command to it to compute an answer, which is itself tagged as a variant value. See the Lecture notes, Section 5.9.3. You should think of programming and proof building as the step-wise application of goal-directed structures to solving a goal. So-called "structure editors" help you do this. (VS is not much of a structure editor. )-: