Skip to content Skip to navigation

Connexions

You are here: Home » Content » homework B solution

Navigation

Recently Viewed

This feature requires Javascript to be enabled.
 

homework B solution

Module by: Ian Barland, John Greiner. E-mail the authors

Summary: (Blank Abstract)

Warning:

The information in this module is outdated. Please see my course for a table of contents.

browser note:

This page meant to be viewed with a MathML-enabled browser. If you see (∀x. (P(x) → (∃y. (P(y) ∨ φ)))) as a nice version of (forall x . (P(x) -> (exists y . (P(y) v phi)))) you're doing okay; If you further see 𝒜 ⊢ ℬ as a nice version of (script-A |- script-B) you're set! If not, either try using mozilla, or check whether there's a .ps or .pdf version of this file available.

Due 2002.Apr.02 (tues).

For proofs on this homework, (ps, pdf) use the inference rules (ps, pdf) and WaterWorld domain axioms (ps, pdf)

Exercise 1

Fill in the blank reasons in the following proof that ∨ commutes (that is, (a ∨ b) ⊢ (b ∨ a)).

  1. (a ∨ b) [premise]
  2. subproof: a ⊢ (b ∨ a)
    1. a [premise for subproof]
    2. (b ∨ a) [∨Intro]
  3. subproof: b ⊢ (b ∨ a)
    1. b [premise for subproof]
    2. (b ∨ a) [________________]
  4. (b ∨ a) [________________ ]
Note that this proof involved the very simple WFFs a, b, but since we assumed nothing specific about those particular propositions this proof readily generalizes to any WFFs 𝒜, ℬ.

Solution

  1. (a ∨ b) [premise]
  2. subproof: a ⊢ (b ∨ a)
    1. a [premise]
    2. (b ∨ a) [∨Intro]
  3. subproof: b ⊢ (b ∨ a)
    1. b [premise]
    2. (b ∨ a) [∨Intro]
  4. (b ∨ a) [∨Elim[𝒜/a][ℬ/b][𝒞/(b ∨ a)], lines 1,2,3]

Exercise 2

Having given this proof of (𝒜 ∨ ℬ) ⊢ (ℬ ∨ 𝒜) in future proofs we can now include as a theorem -- without any premises -- the formula ________________. The justification for this is the ________________ rule of inference.

Of course, this is a bit of a short-cut, since technically "..by previously proven theorem" isn't listed on our sheet of inference rules. If we were playing strictly by the rules, we'd have to repeat the old proof as one big subproof, and then add one extra line (the theorem and inference rule you just mentioned).

But what if we have a previously-written proof with three premises (𝒜, ℬ, 𝒞 ⊢ 𝒵)? In this case, the corresponding theorem is ________________. If we were being strict and not allowing the citing of previous proofs, what steps, exactly, would you need to add to your new proof to make use of this new theorem?

Solution

Having proven (𝒜 ∨ ℬ) ⊢ (ℬ ∨ 𝒜) lets us use the formula ___((𝒜 ∨ ℬ)→(ℬ ∨ 𝒜))___ in later proofs, implicitly using the ___→Intro___ inference rule.

If we'd proven 𝒜, ℬ, 𝒞 ⊢ 𝒵, then the pertinent theorem is ((𝒜 ∧ ℬ ∧ 𝒞)→𝒵); technically you'd insert the following into your current proof:

    1. (𝒜 ∧ (ℬ ∧ 𝒞)) [premise for subproof]
    2. 𝒜 [∧Elim (left)]
    3. (ℬ ∧ 𝒞) [∧Elim (right)]
    4. ℬ [∧Elim (left)]
    5. 𝒞 [∧Elim (right)]
    6. ...[insert the lines of previous proof, renumbering the steps from 6, and replacing "premise" with line 2,4, or 5 as appropriate]...
    7. 𝒵 [(last step of the included proof)]
  2. ((𝒜 ∧ (ℬ ∧ 𝒞))→𝒵) [∧Intro]
It's okay to not worry about the associativity of ∧ (omitting step 1.3); the important point is that there are several technical steps needed of converting multiple premises to a single conjunction, when translating between proofs and theorems (using the technically correct, non-shorthand rules).

Exercise 3

Using the rule of inference RAA, prove ¬a ⊢ ¬(a ∧ b).

Solution

We observe that to use RAA to conclude ¬(a ∧ b) will require a subproof of ¬¬(a ∧ b) ⊢ false. (That is, the rule's 𝒜 refers to a WFF which is already a negation: "¬(a ∧ b)". Not a problem at all.)

  1. ¬a [premise]
    1. ¬¬(a ∧ b) [premise for subproof]
    2. (a ∧ b) [From lecture & newsgroup: ¬Elim, line 2.1]
    3. a [∧Elim, line 2.2]
    4. false [falseIntro, lines 1, 2.3]
  3. ¬(a ∧ b) [RAA[𝒜/¬(a ∧ b)], line 2]

Exercise 4

[*practice]

Show that (¬W-safe ∨ ¬Y-unsafe) ⊢ (W-unsafe ∨ Y-safe).

hint:

use the ∨Elim inference rule to get the final result.

Solution

  1. (¬W-safe ∨ ¬Y-unsafe) [premise]
    1. ¬W-safe [premise for subproof]
    2. (¬W-safe→W-unsafe) [domain axiom relating W-safe, W-unsafe]
    3. W-unsafe [→Elim]
    4. (W-unsafe ∨ Y-safe) [∨Intro]
    ¬W-safe ⊢ (W-unsafe ∨ Y-safe) [recapitulate subproof]
    1. ¬Y-unsafe [premise for subproof]
    2. (¬Y-unsafe→Y-safe) [domain axiom relating Y-safe, Y-unsafe]
    3. Y-safe [→Elim]
    4. (W-unsafe ∨ Y-safe) [∨Intro]
    ¬Y-unsafe ⊢ (W-unsafe ∨ Y-safe) [recapitulate subproof]
  4. (W-unsafe ∨ Y-safe) [ ∨Elim ]

Exercise 5

For the following WaterWorld proof of X-has-1 ⊢ (W-unsafe ∨ Y-unsafe), provide the missing steps and/or reasons:

Aside:

The original version of this problem was filled in with reasons which led to a different conclusion (namely ((W-safe ∧ Y-unsafe) ∨ (W-unsafe ∧ Y-safe))). The proof was correct, but it was a roundabout way of proving something which was nearly a domain axiom already. This version is more interesting, but you can turn in either version for your hw.
  1. X-has-1 [________________]
  2. ________________ [domain axiom X1]
  3. ________________ [→Elim]
    1. (W-safe ∧ Y-unsafe) [premise for subproof]
    2. Y-unsafe [________________]
    3. (W-unsafe ∨ Y-unsafe) [∨Intro]
    (W-safe ∧ Y-unsafe) ⊢ (W-unsafe ∨ Y-unsafe) [recapitulate subproof]
    1. ¬(W-safe ∧ Y-unsafe) [________________]
    2. ________________ [from class (𝒜 ∨ ℬ), ¬𝒜 ⊢ ℬ, substituting [𝒜/________________][ℬ/________________])]
    3. W-unsafe [∧Elim]
    4. ________________ [∨Intro]
    ________________ [ recapitulate subproof ]
  6. ________________ [________________]

Solution

  1. X-has-1 [premise]
  2. (X-has-1→((W-safe ∧ Y-unsafe) ∨ (W-unsafe ∧ Y-safe))) [domain axiom X1]
  3. ((W-safe ∧ Y-unsafe) ∨ (W-unsafe ∧ Y-safe)) [→Elim]
    1. (W-safe ∧ Y-unsafe) [premise for subproof]
    2. Y-unsafe [∧Elim]
    3. (W-unsafe ∨ Y-unsafe) [∨Intro]
    (W-safe ∧ Y-unsafe) ⊢ (W-unsafe ∨ Y-unsafe) [ recapitulate subproof ]
    1. ¬(W-safe ∧ Y-unsafe) [premise for subproof]
    2. (W-unsafe ∧ Y-safe) [from class (𝒜 ∨ ℬ), ¬𝒜 ⊢ ℬ, substituting [𝒜/(W-safe ∧ Y-unsafe)][ℬ/(W-unsafe ∧ Y-safe)])]
    3. W-unsafe [∧Elim]
    4. (W-unsafe ∨ Y-unsafe) [∨Intro]
    ¬(W-safe ∧ Y-unsafe) ⊢ (W-unsafe ∨ Y-unsafe) [ recapitulate subproof ]
  6. (W-unsafe ∨ Y-unsafe) [∨Elim (lines 4,5)]

Exercise 6

Figure 1
Figure 1 (hwA-1.png)

Given the above figure (backup link) (as premises), prove that location P is safe by using our proof system and the WaterWorld domain axioms.

While this proof is longer (about 15 steps), it's not too bad. To make life easier, you may also use the following (mostly from class; as usual 𝒜 and ℬ stand for any WFF):

  • ¬𝒜 ⊢ ¬(𝒜 ∧ ℬ)
  • The theorem   ⊢ (((𝒜 ∨ ℬ) ∧ ¬𝒜)→ℬ) Hint: If you have a formula of the form (𝒟 ∨ (ℰ ∨ ℱ)) you can use this rule twice in succession.

    Aside:

    When using a domain axiom which mentions a disjunction or conjunction of three items (technically not a WFF), you can choose whichever fully-parenthesized version you like. (You can consider those domain axioms which use three-way disjunction/conjunctions as shorthand for two separate domain axioms, the left- and right-associative versions.)
  • (Q-has-1→((P-safe ∧ R-safe) ∨ (P-safe ∧ W-safe) ∨ (R-safe ∧ W-safe))). Okay, this wasn't presented in class, but it's similar in spirit to Exercise 5, so you can feel confident that we're not pulling one over on you.
  • Not only is Y-safe an allowable premise (reading off the given board), but so is ¬Y-unsafe.

Solution

  1. Q-has-1 [premise]
  2. X-has-1 [premise]
  3. ¬Y-unsafe [premise]
  4. (X-has-1→(Y-unsafe ∨ W-unsafe)) [th'm: previous problem (and, →Intro).]
  5. (W-unsafe ∨ Y-unsafe) [→Elim, lines 2 and 4.]
  6. (Y-unsafe ∨ W-unsafe) [Exercise 1: ∨ commutes; line 5.]
  7. W-unsafe [Th'm from class: ¬𝒜, (𝒜 ∨ ℬ) ⊢ ℬ, lines 3,6.]
    1. ¬¬(P-safe ∧ W-safe) [premise for subproof]
    2. (P-safe ∧ W-safe) [From lecture & newsgroup: ¬Elim, line 8.1]
    3. W-safe [∧Elim]
    4. (W-safe→¬W-unsafe) [domain axiom relating W-safe, W-unsafe]
    5. ¬W-unsafe [→Elim, lines 8.2, 8.3]
    6. false [falseIntro, lines 7, 8.4]
  9. ¬(P-safe ∧ W-safe) [RAA, line 8]
    1. ¬¬(R-safe ∧ W-safe) [premise for subproof]
    2. (R-safe ∧ W-safe) [From lecture & newsgroup: ¬Elim, line 10.1]
    3. W-safe [∧Elim]
    4. (W-safe→¬W-unsafe) [domain axiom relating W-safe, W-unsafe]
    5. ¬W-unsafe [→Elim, lines 10.2, 10.3]
    6. false [falseIntro, lines 7, 10.4]
  11. ¬(R-safe ∧ W-safe) [RAA, line 10]
  12. (Q-has-1→(((P-safe ∧ R-safe) ∨ (P-safe ∧ W-safe)) ∨ (R-safe ∧ W-safe))) [Allowed by problem statement (similar to Exercise 5).]
  13. (((P-safe ∧ R-safe) ∨ (P-safe ∧ W-safe)) ∨ (R-safe ∧ W-safe)) [→Elim, lines 1,12.]
  14. ((R-safe ∧ W-safe) ∨ ((P-safe ∧ R-safe) ∨ (P-safe ∧ W-safe))) [Th'm: ∨ commutes (ex.1), line 13.]
  15. ((P-safe ∧ R-safe) ∨ (P-safe ∧ W-safe)) [Th'm from class: ¬𝒜, (𝒜 ∨ ℬ) ⊢ ℬ, lines 9,14.]
  16. ((P-safe ∧ W-safe) ∨ (P-safe ∧ R-safe)) [Th'm: ∨ commutes (ex.1), line 15.]
  17. (P-safe ∧ R-safe) [Th'm from class: ¬𝒜, (𝒜 ∨ ℬ) ⊢ ℬ, lines 11,16.]
  18. P-safe [∧Elim -- Whew!]
The sub-proofs 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.

note:

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.)

Exercise 7

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 theorem ((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 transliterated to P,U,W,X (resp.)? If you replace such steps with the closest true statements you can ("translating" instead of "transliterating", if you will), where is the first line of the proof which fails and cannot be patched?

Solution

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.

A direct substitution of B,G,J,K with P,U,W,X leads to a faulty statement in lemma B, line 5: The domain axiom B1 has as its conclusion that there is exactly one pirate in A and C, while the domain axiom P1 is not exactly analagous: it's conclusion is exactly one pirate in N,Q,H. So a correct translation would have the correct domain axiom P1.

This isn't (yet) catastrophic; 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 ((𝒜 ∨ ℬ), ¬𝒜); we can't translate the reasoning to end up with a single conjunction like (N-safe ∧ H-safe ∧ Q-unsafe).

Can the proof be patched, by somehow twiddling with ∧'s associativity, or extending the theorem to handle disjunctions with three terms? No -- we realize that we have a counterexample above, and since our logic is sound there can't be a proof of the statement; in particular it's this line (lemma B, line 8) of the proof that fundamentally can't be repaired.

Exercise 8

Sketch a board and an accompanying (simple) WFF where you know the formula is true, but it's not possible to prove it using the WaterWorld domain axioms.

hint:

Use a board where knowing the (total) number of pirates is needed to solve the puzzle.

Solution

Figure 2
Figure 2 (z-safe.png)

Consider a board where there is only one pirate, and it's already been discovered at location Y. There is no domain axioms which let us deduce that Z-safe. Observer that the proposition totCount-is-1 is true for this board.

Exercise 9

The preceding difficulty arises from the fact that we don't have any domain axioms dealing with the pirate count (even though we have propositions involving it).

We call this WaterWorld logic incomplete, since we can write sentences that are true but don't have proofs. Clearly, this is a shortcoming of the WaterWorld proof system!

Aside:

If we'd never included propositions involving the number of remaining pirates, we'd have a complete proof system -- but we wouldn't be able to fully express all the pertinent knowledge we use in our real-life reasoning about the board! In general, there is a balance between expressiveness, and desirable properties likes completeness.

In this case though, it's easy to shore up the system by adding some domain axioms (which are clearly independent from the rest). Give a new domain axiom which helps prove true statements not previously provable, in boards where the total pirate count is 1. (Use "..." as needed, for repetitious parts). (There are many possible answers here.) Similarly for boards where the total pirate count is 2. (To think to yourself: about how many such new rules are needed, just for boards with a pirate count of 5?)

Aside:

Remember that our WaterWorld vocabulary only deals with the underlying state of the game, not with the view of the game. There are no propositions dealing with whether location A has been revealed or not; instead we recognize that some proofs use A-safe as a premise and some don't.

Solution

One formula that would have helped in the above board is: ((totCount-is-1 ∧ Y-unsafe)→(A-safe ∧ B-safe ∧ ... ∧ W-safe ∧ Z-safe)). Adding this as a domain axiom would be a big help. Similarly, 24-1 = 23 other domain axioms are needed (involving not just Y-unsafe, but any unsafe location). Does this set of domain axioms gives us a complete logic for boards with totCount-is-1? Hopefully, but proving this is much more difficult!

note:

If we add only domain axioms which let us conclude the safety of locations F and Z, that's not enough to give us completeness: Consider the board where only one location (near the middle) is revealed, and it's revealed as a pirate (an undeservedly lucky first guess, perhaps). Then that's still enough to solve the board, even though locations F and Z aren't unusally pertinent.

Instead, one could add the single (long) domain axiom (totCount-is-1→((A-unsafe ∧ B-safe ∧ C-safe ∧ ... ∧ Z-safe) ∨ (A-safe ∧ B-unsafe ∧ C-safe ∧ ... ∧ Z-safe) ∨ ... ∨ (A-safe ∧ B-safe ∧ C-safe ∧ ... ∧ Y-safe ∧ Z-unsafe))). How might you show that adding this one domain axiom is equivalent to adding the 23 previously-mentioned domain axioms?

For boards with a total of two pirates, we can add 24-choose-2 domain axioms of the form ((totCount-is-2 ∧ A-unsafe ∧ B-unsafe)→(C-safe ∧ D-safe ∧ ... ∧ Z-safe)), and so on for all pairs of locations being unsafe. Alternately, one long rule (totCount-is-1→((A-unsafe ∧ B-unsafe ∧ C-safe ∧ ... ∧ Z-safe) ∨ ...)). Again, how might you show these two approaches are equivalent? And, is this enough to give us an complete logic? Again this seems plausible, but even more than in the single case it seems there might be boards where there is a deduction which can be made, but our domain axioms don't cover it.

Extending this system gives 24-choose-5 (over 40,000) domain axioms or one rule with that-many clauses. And if you want your domain axioms to cover any number of pirates, you'll need 2^25 (over 30 million) domain axioms or clauses. All this, just for a fixed-size board! This emphasizes just how poor a language we have, for modeling WaterWorld. But we'll see a price paid for a better description (one which can deal with numbers directly): we'll have to give up completeness!

note:

It's conceivable (though not obvious how) to have a system which is incomplete, but no matter how you shore it up with new domain axioms you still have a proof system that's incomplete.

Exercise 10

Rosen, section 6.1 problem 2: For the relation "divides" on the set {1,2,3,4,5,6}:

  • List all the ordered pairs in the relation.
  • Display the relation graphically.
  • Display the relation in tabular form.

Solution

  • List all the ordered pairs in the relation: {(1,2), (1,3), (1,4), (1,5), (1,6), (2,2), (2,4), (2,6), (3,3), (3,6), (4,4), (5,5), (6,6)}
  • Display the relation graphically: Note that you can collapse the two nodes of each pair, and the direction of the arrow preserves all the information.

    todo:

    peggy ?
  • Display the relation in tabular form: (see table)
Table 1: Tabular form for "divides?"
\\123456
1XXXXXX
2 X X X
3 X X
4 X
5 X
6 X

Exercise 11

Rosen, section 6.1 problem 4: Determine whether, for the domain of all people, the following relations are reflexive, symmetric, antisymmetric, transitive.

  • taller?
  • bornSameDay?
  • sameFirstName?
  • commonGrandparent?

Solution

  • taller?: antisymmetric, transitive
  • bornSameDay?: reflexive, symmetric, transitive.
  • sameFirstName?: reflexive, symmetric, transitive.
  • commonGrandparent?: reflexive, symmetric.

Exercise 12

While Rosen discusses binary relations (subsets of pairs), one can also have unary relations (subsets of the domain -- e.g. isPrime? for numbers), and ternary relations (subsets of triples -- e.g. isAChildOf? over the domain of people.)

Suppose you wanted to encode addition as a ternary relation "addsTo?" over (triples of) numbers -- describe briefly what triples (x,y,z) would be in the relation; give an example of a triple in the relation addsTo? and a triple not in the relation addsTo?.

(Note that in general, you can turn any k-ary function into a (k+1)-ary relation. )

Solution

A natural way of encoding addition is with the ternary relation addsTo? = { (x, y, z) | x+y=z }. That is, the set of triples where the first two happen to add to the third. Thus (3,4,7) is in the set addsTo?, but (3,4,8) and (7,4,3) aren't.

note:

You could have a different relation encode the same information. For example, where the middle element is the other two elements added, then squared. Tuples where the middle item wasn't a perfect square may or may not be in the relation, and wouldn't contribute to denoting valid information about sums. (That's presuming the domain was integers.)

Content actions

Download module as:

PDF | EPUB (?)

What is an EPUB file?

EPUB is an electronic book format that can be read on a variety of mobile devices.

Downloading to a reading device

For detailed instructions on how to download this content's EPUB to your specific device, click the "(?)" link.

| More downloads ...

Add module to:

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

Definition of a lens

Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

Who can create a lens?

Any individual member, a community, or a respected organization.

What are tags? tag icon

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks