Reasoning with Inference Rules For proofs on this homework, Remember that each step must be justified by one of: "premise", a listed inference rule (.ps) (a previous line number and, if ambiguous, substitutions for the inference rule's metavariables), or a WaterWorld domain axiom. (Carried over from original hw01 assignment.) (2 pts.) Fill in the blank reasons in the following proof that ∨ commutes, that is, χ ∨ υ ⊢ υ ∨ χ. 1χ ∨ υ premise 2subproof:χ ⊢ υ ∨ χ 2.a χ premise for subproof 2.b υ ∨ χ ∨Intro 3subproof:υ ⊢ υ ∨ χ 3.a υ premise for subproof 3.b υ ∨ χ ____________ 4υ ∨ χ ____________

(5pts.) Show that τ ∧ χτ → υχ → ω ⊢ υ ∧ ω. (It may take around 8 steps.) (4pts) Using the inference rule RAA, prove ¬χ ⊢ ¬χ ∧ υ. (6pts.) Show that ¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe. Use the ∨Elim inference rule to get the final result. (5pts) For the following WaterWorld proof of X-has-1 ⊢ W-unsafe ∨ Y-unsafe, provide the missing steps and/or reasons: 1X-has-1 ____________ 2____________ WaterWorld domain axiom 3____________ →Elim 4subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe 4.a W-safe ∧ Y-unsafe premise for subproof 4.b Y-unsafe____________ 4.c W-unsafe ∨ Y-unsafe ____________ 5subproof:¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe 5.a ¬W-safe ∧ Y-unsafe premise for subproof 5.b W-unsafe ∧ Y-safe CaseElim (left), where φ=____________, and ψ=____________. 5.c ____________ ____________ 5.d W-unsafe ∨ Y-unsafe ____________ 6W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeFrom class, φ ∨ ¬φ, with φ____________ 7W-unsafe ∨ Y-unsafe ____________

[practice; 0pts]

A sample WaterWorld board Given the above figure, and using any of the immediately obvious facts as premises, prove that location P is safe by using our proof system and the WaterWorld domain axioms. While this proof is longer (nearly 30 steps), it's not too bad. To make life easier, you may also use the following: ¬φ ⊢ ¬φ ∧ ψ Q-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe. Not only is Y-safe an allowable premise (reading off the given board), but so is ¬Y-unsafe. 1Q-has-1 premise 2X-has-1 premise 3¬Y-unsafe premise 4X-has-1 → Y-unsafe ∨ W-unsafeth'm: previous problem (and, →Intro) 5W-unsafe ∨ Y-unsafe →Elim, by lines 2,4 6Y-unsafe ∨ W-unsafe ∨ commutes; line 5 7W-unsafe CaseElim, by lines 3,6 8subproof:¬¬P-safe ∧ W-safe ⊢ 8.a ¬¬P-safe ∧ W-safe premise for subproof 8.b P-safe ∧ W-safe ¬Elim, by line 8.1 8.c W-safe ∧Elim 8.d W-safe → ¬W-unsafe WaterWorld domain axiom 8.e ¬W-unsafe →Elim, by lines 8.2,8.3 8.f Intro, by lines 7,8.4 9¬P-safe ∧ W-safe RAA, by line 8 10subproof:¬¬R-safe ∧ W-safe ⊢ 10.a ¬¬R-safe ∧ W-safe premise for subproof 10.b R-safe ∧ W-safe ¬Elim, by line 10.1 10.c W-safe ∧Elim 10.d W-safe → ¬W-unsafe WaterWorld domain axiom 10.e ¬W-unsafe →Elim, by lines 10.2,10.3 10.f Intro, by lines 7,10.4 11¬R-safe ∧ W-safe RAA, by line 10 12Q-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe Allowed by problem statement 13P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe →Elim, by lines 1,12 14R-safe ∧ W-safe ∨ P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ commutes (ex.1), by line 13 15P-safe ∧ R-safe ∨ P-safe ∧ W-safe CaseElim, by lines 9,14 16P-safe ∧ W-safe ∨ P-safe ∧ R-safe Theorem: ∨ commutes (ex.1), line 15. 17P-safe ∧ R-safe CaseElim, by lines 11,16. 18P-safe∧Elim -- Whew!

The subproofs could easily have been pulled out into lemmas (making the proof clearer, exactly as subroutines make programs clearer, even if only called once). Observe how the second subproof had to repeat lines identical from the first -- it would have been incorrect to cite those earlier subproof lines, because the previous subproof had been completed. Interestingly, we didn't need to use R-safe as a premise. (In fact, we nearly proved that ¬R-safe would have been inconsistent with the other premises.) (6 pts) State where on a board pirates could be positioned, so that: P-has-1 ∧ U-has-1 ∧ W-has-1, but X-safe. Compare this with a previous theorem (example 11) B-has-1 ∧ G-has-1 ∧ J-has-1 → K-unsafe, the same idea shifted down a couple of rows. Suppose we try to translate this proof so as to conclude ¬X-safe (clearly untrue, by the above). What is the first step of the proof which doesn't hold when B,G,J,K are replaced with P,U,W,X, respectively? (Just give a line number; no explanation needed. Your answer will be of the form "Lemma A line 1" or "main proof line 2".) If you replace such steps with the closest true formulas you can ("translating" instead of "transliterating", if you will), "transliterate" meaning a word-for-word substitution, while "translation" tries to preserve meanings/idioms. So, the German "Übung macht den Meister" transliterates to "Drill makes the master", but translates to "practice makes perfect". where is the first line of the proof which fails and cannot be patched? (Just give a line number; no explanation needed. Your answer will be of the form "Lemma A line 1" or "main proof line 222".) (Extra Credit 3 pts) Describe a board and an accompanying (simple) WFF where you know the formula is true, yet it's not possible to prove it via the WaterWorld domain axioms without mentioning propositions about the total-pirate-count totCount-is-1, totCount-is-2, …. (Indeed, you may have noticed that list of domain axioms makes only a paltry attempt at including domain axioms involving totCount-is-5. There are quite a few omitted subcases as it is, even without considering other total-pirate-counts.) As always, a simpler example is better. Suppose we don't patch up the WaterWorld domain axioms with numerous axioms for each of the total-pirate-count cases. What does your example above say about the soundness and the completeness of our WaterWorld domain axioms? (Recall that the pertinent problem when playing waterworld is not that you sometimes have to guess, but rather knowing whether a guess is the only option.)