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υ ∨ χ ____________

Line 3b justification: ∨Intro, by line 3a. Line 4 justification: ∨Elim, by lines 1,2,3, where φ=χ and ψ=υ and θ=υ ∨ χ (5pts.) Show that τ ∧ χτ → υχ → ω ⊢ υ ∧ ω. (It may take around 8 steps.) This is basically just two instances of →Elim, plus a little manipulation of ∧. 1τ ∧ χ premise 2τ ∧Elim (left), by line 1, where φ=τ and ψ=χ 3τ → υ premise 4υ →Elim, by lines 2,3, where φ=τ and ψ=υ 5χ ∧Elim (right), by line 1, where φ=τ and ψ=χ 6χ → ω premise 7ω →Elim, by lines 5,6, where φ=χ and ψ=ω 8υ ∧ ω ∧Intro, by lines 4,7, where φ=υ and ψ=ω

(4pts) Using the inference rule RAA, prove ¬χ ⊢ ¬χ ∧ υ. We observe that to use RAA to conclude ¬χ ∧ υ will require a subproof of ¬¬χ ∧ υ ⊢ . (That is, the rule's φ refers to a WFF which is already a negation: "¬χ ∧ υ". Not a problem at all.) 1¬χ premise 2subproof:¬¬χ ∧ υ ⊢ 2.a ¬¬χ ∧ υ premise for subproof 2.b χ ∧ υ ¬Elim, by line 2.1 2.c χ ∧Elim, by line 2.2 2.d Intro, by lines 1,2.3 3¬χ ∧ υ RAA, by line 2, where φ=¬χ ∧ υ

(6pts.) Show that ¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe. Use the ∨Elim inference rule to get the final result. 1¬W-safe ∨ ¬Y-unsafe premise 2subproof:¬W-safe ⊢ W-unsafe ∨ Y-safe 2.a ¬W-safe premise for subproof 2.b ¬W-safe → W-unsafeWaterWorld domain axiom 2.c W-unsafe →Elim 2.d W-unsafe ∨ Y-safe ∨Intro 3subproof:¬Y-unsafe ⊢ W-unsafe ∨ Y-safe 3.a ¬Y-unsafe premise for subproof 3.b ¬Y-unsafe → Y-safe WaterWorld domain axiom 3.c Y-safe →Elim 3.d W-unsafe ∨ Y-safe ∨Intro 4W-unsafe ∨ Y-safe ∨Elim

(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 ____________

Since Step 4 is of the form φ → θ, and Step 5 is of the form ¬φ → θ, this is enough to prove θ by ∨Elim, once we include (from class) φ ∨ ¬φ. 1X-has-1 premise 2X-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe WaterWorld domain axiom 3W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe →Elim 4subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe 4.a W-safe ∧ Y-unsafe premise for subproof 4.b Y-unsafe ∧Elim 4.c W-unsafe ∨ Y-unsafe ∨Intro 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 φ=W-safe ∧ Y-unsafe, and ψ=W-unsafe ∧ Y-safe 5.c W-unsafe ∧Elim 5.d W-unsafe ∨ Y-unsafe ∨Intro 6W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeFrom class, φ ∨ ¬φ, with φW-safe ∧ Y-unsafe 7W-unsafe ∨ Y-unsafe ∨Elim, by lines 5,6, with φW-safe ∧ Y-unsafe ψ¬W-safe ∧ Y-unsafe θW-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".) You could have pirates at H and V, (and, no pirates at X, N, or Q), and still have P-has-1 ∧ U-has-1 ∧ W-has-1, be true on the given board. Lemma B, line 5: After a direct substition, the formula we obtain isn't an actual domain axiom any more. The domain axiom B1 had as its conclusion that there is exactly one pirate in A and C, while the domain axiom P1 is not exactly analogous: its conclusion is exactly one pirate in N,Q,H. So a translation should really use the correct domain axiom P1. Lemma B, line 8: By patching line 5 we can still continue to step 6, inferring a disjunction with 3 terms, still using →Elim (namely, H-safe ∧ N-safe ∧ Q-unsafe ∨ H-safe ∧ N-unsafe ∧ Q-safe ∨ H-unsafe ∧ N-safe ∧ Q-safe). The fundamental problem comes up in line 8: we can't apply the cited theorem (φ ∨ ψ ⊢ ¬φ). There's no obvious way to patch it to still end up with a single conjunction like N-safe ∧ H-safe ∧ Q-unsafe. We wonder whether, if we're clever enough and somehow twiddle ∧'s associativity or we extend the theorem to handle disjunctions with three terms, if we can get the desired result? No -- we realize that we have a counterexample above, and since our logic is sound there can't be a proof of the formula; in particular it's this line (lemma B, line 8) of the proof that fundamentally can't be repaired. (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.)

A sample WaterWorld board Consider a board shown by the above figure, where there is only one pirate, and it's already been discovered at location Y. There are no domain axioms which let us deduce that Z-safe. Observe that the proposition totCount-is-1 is true for this board. This means that our WaterWorld domain axioms are incomplete: there are true facts that cannot be deduced. In this case, it's possible to patch up our system by adding more domain axioms. (I'll leave it to you to think about how many rules you might need, for propositional logic.)

Relations and Interpretations (5 pts) Are each of the following formulas true for all interpretations ("valid")? (Remember that the relation-names are just names in the formula; don't assume the name has to have any bearing on their interpretation.) For arbitrary a,b in the domain, atLeastAsWiseAsab ∨ atLeastAsWiseAsba For arbitrary a in the domain, primea → odda → primea For arbitrary a,b in the domain, betterThanab → ¬betterThanba For each, if it is true or false under all interpretations, prove that. (For these small examples, a truth table will probably be easier than using boolean algebra or an inference-system proof.) Otherwise, give and interpretation in which it is true, and one in which it is false. As always, look at trivial and small test cases first. Here, try domains with zero, one, or two elements, and small relations. Not valid. The formula atLeastAsWiseAsab ∨ atLeastAsWiseAsba is false when the domain is {apple} and the relation atLeastAsWiseAs = {}. However it is true for the same domain but interpreting atLeastAsWiseAs = {apple apple}. Valid. Choose any interpretation you like, and we'll show that primea → odda → primea is true. Let P be the truth value of primea under that interpretation, and similarly and let Q be the truth value of odda. Then (for that interpretation) the original formula has the truth value P → Q → P, which is a tautology back in propositional logic (truth table below), and so the original formula is true under all interpretations. Not valid. The formula betterThanab → ¬betterThanba is false when the domain is {apple} and betterThan is interpreted as {apple apple}. This formula is true when the domain is the empty relation {}. (In general, it is true whenever betterThan is interpeted as a antisymmetric relation which is nowhere reflexive.) Truth-table for propositional analog of a relational formula. PQP → Q → P

Fortunately, none of these three formulas turned out to be unsatisfiable, else it sure would have been hard to give an example which where it did hold. (Taking the negation of a valid formula will give you an unsatisfiable one.)