Skip to content Skip to navigation

Connexions

You are here: Home » Content » comp280 hw03 solution

Navigation

Content Actions
  • Download module PDF
  • Add to ...
    Add the module to:
    • My Favorites
    • A lens
    • An external social bookmarking service
    • My Favorites (What is 'My Favorites'?)
      'My Favorites' is a special kind of lens which you can use to bookmark modules and collections directly in Connexions. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need a Connexions account to use 'My Favorites'.
    • A lens (What is a lens?)

      Definition of a lens

      Lenses

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

      What is in a lens?

      Lens makers point to Connexions 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 Connexions 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
  • E-mail the author
  • Rate this module (How does the rating system work?)

    Rating system

    Ratings

    Ratings allow you to judge the quality of modules. If other users have ranked the module then its average rating is displayed below. Ratings are calculated on a scale from one star (Poor) to five stars (Excellent).

    How to rate a module

    Hover over the star that corresponds to the rating you wish to assign. Click on the star to add your rating. Your rating should be based on the quality of the content. You must have an account and be logged in to rate content.

    		(0 ratings)

Recently Viewed

This feature requires Javascript to be enabled.

comp280 hw03 solution

Module by: Ian Barland

Summary: Solutions for hw03, comp280 04spring.

Note: Your browser may not currently support MathML. See our browser support page for additional details. You can always view the correct math in the PDF version.

Exercise 1

(2pts) Add yourself to the online grade-database. This part is due by Monday Feb.09, 17:00, so that we can return earlier homeworks to you in class on Tuesday 10th!

Solution

You can check your grades on-line . Check this regularly throughout the semester, and inform us right away if there is a discrepancy. The link is also available on the class homework page.

First-order logic

Exercise 2

(3 pts.) Rosen, Section 1.3, pg.44, #58.

N.B.:

Carried over from original hw02 assignment.

Hint:

Express all formulas using ∀∀, to make your life easier for part (d).
  1. No ducks are willing to waltz.
  2. No officers ever decline to waltz.
  3. All my poultry are ducks.
  4. My poultry are not officers.
  5. Does (d) follow from (a), (b), (c) ? Argue informally; you don't need to use the algebra or inference rules for first-order logic here.

Solution

  1. ∀x. Px → ¬Sx∀x.Px → ¬Sx
  2. ∀x. Rx → Sx∀x.Rx → Sx
  3. ∀x. Qx → Px∀x.Qx → Px
  4. ∀x. Qx → ¬Rx∀x.Qx → ¬Rx
  5. Since all statements are universal, i.e. in terms of the forall quantifier, we can drop it for ease in our deduction. (a) and (c) will give us the statement Qx → ¬SxQx → ¬Sx. We rewrite (b)'s innards to its contrapositive, ∀x. ¬Sx → ¬Rx∀x.¬Sx → ¬Rx. Combining this with what we deduced, we conclude that Qx → ¬RxQx → ¬Rx, which is what we claim in (d).

Exercise 3

(4pts) You come home one evening to find your roommate exuberant because they have managed to prove that there is an even prime numbers bigger than two. More precisely, they have a correct proof of ∃y.Py ∧ y>2 → Ey∃y.Py ∧ y2 → Ey , for the domain of natural numbers with PP interpreted as "is prime?" and EE interpreted as "is even?". While they are celebrating their imminent fame at this amazing mathematical discovery, you ponder…

  • …and realize the formula is indeed true for that interpretation. Briefly explain why. (You don't need to give a formal proof using inference rules or boolean algebra; just give a particular value for yy and explain why it does satisfy the body of "∃y.∃y.".)
  • Is their formula still true, when restricted to the domain of natural numbers two or less? (Using the same interpretation of PP, EE. Briefly explain why.
  • Is their formula still true, when restricted to the empty domain? Briefly explain why.
  • Give a formula that does actually capture the notion "there is an even prime number bigger than 2".

Solution

  • By choosing the witness y=4y 4, we see that Py ∧ y>2Py ∧ y2 is not true, therefore Py ∧ y>2 → EyPy ∧ y2 → Ey does hold. (Recall how false → true ≡ true → ≡, by →→'s truth-table ). Since there does exist a value for yy satisfying the inner formula, so the existential formula is true.
  • Yes -- restricted to the smaller domain, we see that choosing any value 2 or less for yy also makes the formula is true, as in the previous part.
  • It is not true on the empty domain, since ∃y.φ∃y.φ is false for any formula φφ.

Exercise 4

(Extra Credit 2 pts) For the sentence ∀x. ∀y. Ax ∧ Bxy → Ay∀x.∀y.Ax ∧ Bxy → Ay state whether it is true or false, relative to the following interpretations:

  1. The domain of the natural numbers, where AA is interpreted as "even?" and BB is interpreted as "equals"
  2. The domain of the Booleans (just {true, false}), where AA is interpreted as "false?" and BB is interpreted as "equals"
  3. The domain of WaterWorld locations in the particular board where locations Y and Z contain pirates, but all other locations are safe, and the relation symbol AA is interpreted as "safe?" and BB is interpreted as "neighbors"
  4. All WaterWorld boards, where AA is interpreted as "safe?" and BB is interpreted as "neighbors". (That is, is the formula valid for WaterWorld?)

Solution

  1. fixed:
    true
  2. true
  3. false (Though if AA were interpreted as "unsafe?", this would be true on this board.)
  4. false

Exercise 5

(5pts) Translate the following conversational English statements into first-order logic, using the suggested predicates, or inventing appropriately-named ones if none provided. (You may also freely use = which we'll choose to always interpret as equality.) For the WaterWorld problems, use the set of locations as the domain, and use predicates nhbrnhbr (binary), and unary predicates hasPiratehasPirate, shows3shows3, shows2shows2, shows1shows1, shows0shows0.

  1. "All books rare and used". This is claimed by a local bookstore; what is the intended domain? Do you believe they mean to claim "all books rare or used"?
  2. "Everybody who has truly been kidnapped by a UFO knows that Agent Mulder is alive." (Is this true, presuming that no UFOs have actually visited Earth…yet?)
  3. "In WaterWorld, location λλ has exactly one neighbor." (Your answer will be a formula with λλ free, just as in the notes we developed formulas like "nn is prime" where nn was free.)
  4. "If a WaterWorld location shows a 3, then any neighboring location is a pirate." (This is only true for certain boards.)
  5. "If a WaterWorld location shows a 1, and has exactly one neighbor, then that neighbor has a pirate." Re-use existing code!

Solution

  1. ∀b. rareb ∧ usedb∀b.rareb ∧ usedb . The implicit domain is the books in their shop. It's not clear to me, but I suspect the intended statement is ∀b. rareb ∨ usedb ∧ ∃b.rareb ∧ ∃b.usedb ∀b. rareb ∨ usedb ∧ ∃b.rareb ∧ ∃b.usedb .
  2. Using aa for "abductee", we have ∀a. kidnappeda → knowsIsAliveaAgentMulder∀a.kidnappeda → knowsIsAliveaAgentMulder This is indeed vacuously true -- for all values of aa, kidnappedakidnappeda is false, so the implication holds.
  3. "There exists a neighbors, but not two unique neighbors": ∃m. nhbrλm ∧ ¬ ∃m. ∃n. nhbrλm ∧ nhbrλn ∧ m≠n ∃m. nhbrλm ∧ ¬ ∃m. ∃n. nhbrλm ∧ nhbrλn ∧ m n , interpreted over the domain of WaterWorld locations. (To think about: does this allow for a location to be its own, only neighbor?)
  4. ∀x. shows3x → ∀y. nhbrxy → hasPiratey ∀x.shows3x → ∀y. nhbrxy → hasPiratey
  5. fixed:
    Original sol'n talked about two neighbors, not one.
    ∀l. shows1l ∧ hasExactly1Nhbrl → ∃m. nhbrlm ∧ hasPiratem ∀l.shows1l ∧ hasExactly1Nhbrl → ∃m. nhbrlm ∧ hasPiratem , where really "hasExactly1NhbrlhasExactly1Nhbrl" is shorthand for the entire formula from part (c) above. Admittedly, it's a bit strange, to have the hasExactly1NhbrhasExactly1Nhbr part of the formula locate and identify the unique neighbors, and then we forget about them and re-find "∃m.∃n.…∃m.∃n.…". Alternately you could take your hasExactly1NhbrhasExactly1Nhbr formula and change it so that it also asserts that the located neighbor has a pirate. In general, it's probably easier to re-use your existing formula, for both writing the concept and for wondering whether it's correct.

Exercise 6

(Extra Credit 2pts) Write a formula that is the conjunction of

  1. All for one, and one for all!
  2. If you're not for us, you're against us.
  3. The enemy of your enemy is your friend.
  4. Somebody has an enemy. (Not sure of an aphorism expressing this. Maybe, ``Life's not a bed of roses''?)
Use just the relations isForisFor, and isAgainstisAgainst, both to be interpreted on pairs of people. Clarifying some of the ambiguous English:
  • We'll take "one" to mean "one particular person". 1
  • For "us", we'll take it to mean "any one particular individual". You can think of it as each person saying to each other, "if you're not for me, you're against me". Similarly for "you". This captures the intent of the English -- these sayings are meant to apply to everybody, not just one particular person.
  • "your enemy" will mean "somebody you are against", and "your friend" will mean "somebody you are for". (Careful -- this may be different than "somebody who is against/for you").

Aside:

For clarity feel free to express the formula in parts: "φ1 ∧ φ2 ∧ φ3 ∧ φ4φ1 ∧ φ2 ∧ φ3 ∧ φ4, where φ1φ1 = …, φ2φ2 = …, …." This is akin simplifying code into subroutines -- even in situations where you don't call the subroutine more than once, it still adds clarity. You don't have to split up your answer like this; some people might want to have quantifiers that span all four concepts; that's okay, though still strive for an formula that clearly corresponds to the question.

Solution

The solution is ψ1 ∧ ψ2 ∧ ψ3 ∧ ψ4ψ1 ∧ ψ2 ∧ ψ3 ∧ ψ4 where

  1. "All for one and one for all": Thinking "mm" for "martyr" and "pp" for "popular", ψ1 ≡ ∃p.∀x. isForxp ∧ ∃m.∀x. isFormx ψ1≡∃p.∀x. isForxp ∧ ∃m.∀x. isFormx
  2. "If you're not for us, you're against us": ψ2 ≡ ∀x.∀y. ¬ isForxy → isAgainstxyψ2≡∀x.∀y.¬ isForxy → isAgainstxy
  3. "The enemy of your enemy is your friend": ψ3 ≡ ∀y.∀e.∀a. isAgainstye ∧ isAgainstea → isForyaψ3≡∀y.∀e.∀a.isAgainstye ∧ isAgainstea → isForya (Mnemonics: "yy" for "you", "ee" for "enemy", "aa" for "ally".)
  4. "Somebody has an enemy": ψ4 ≡ ∃a.∃b. isAgainstabψ4≡∃a.∃b.isAgainstab

Exercise 7

(Extra Credit 2pts) For the four-part "Musketeer" formula from the preceding exercise, find two (fundamentally different) interpretations of isForisFor which satisfy the formula on a domain of three people.

Depict each of these interpretations as a graph -- draw three circles (nodes) representing the three people, and an arrow (edge) from a person to each person they like. (You can glance at Rosen p.542 (Section 8.1), Figure 8 for one such example of a graph.)

Solution

For a domain of three people, it turns out there are only two (non-isomorphic) interpretations. Take the domain {AA,BB,CC}. Since there are two relations (isForisFor, isAgainstisAgainst), in general we'd need to draw two superposed sets of edges (maybe in different colors, for clarity).

One possible interpretation: both relations are "complete", that is involve all possible pairs: isForisFor = isAgainstisAgainst = { AAAA,ABAB,ACAC, BABA,BBBB,BCBC, CACA,CBCB,CCCC }. Note that this wouldn't work if ψ2ψ2 were strengthened to say "...and furthermore, if you're not against us, then you're for us."

If we voluntarily impose that isForisFor must be the complement of isAgainstisAgainst, we are left with only two possibilities (up to renaming AA,BB,CC): [Pictures soon, hopefully.]

AA is both popular and a martyr: isForisFor = { AAAA,ABAB,ACAC, BABA,BBBB, CACA, CCCC }. isAgainstisAgainst = {BCBC, CBCB}. [Pictures soon, hopefully.]

AA is popular and CC is a martyr: isForisFor = { AAAA, ACAC, BABA,BBBB, CACA,CBCB,CCCC }. isAgainstisAgainst = { ABAB, BCBC }.

Exercise 8

(7pts) Translate the following statements into first-order logic. The domain is to be natural numbers, and the binary relation kthknkthkn indicates whether or not the kkth number of the sequence is nn. That is, for the sequence <5,7,5>, the corresponding relation kthkth is {(1,5), (2,7), (3,5)}. You can also use the binary relations ==, <<, and/or <=<= but no others.

  1. The sequence is finite.
  2. The sequence contains three unique numbers

    Note:

    Containing three numbers doesn't preclude it containing more than three.
  3. The sequence is sorted. (What, exactly, does your formula "sorted" capture -- ascending, descending; allowing duplicates (i.e. non-decreasing or non-increasing)? Any of those four are fine, but say which yours is.)
  4. The sequence is sorted except for (up to) one location. (For example, the sequence < 20, 30, 1, 40, 50 >.)

Solution

  1. The sequence is finite if there exists some last valid index ll, which in turn means "there is a last index ll, such that for all indices ii beyond ll, there is no value at ii." ∃l. ∀i. ¬ ∃n. kthin ∃l.∀i.¬ ∃n. kthin . Turning the inner ¬∃¬∃ into a ∀∀ might make this clearer for some: ∃l. ∀i. ∀n. ¬kthin∃l.∀i.∀n.¬kthin .
  2. ∃a. ∃b. ∃c. ∃i. ∃j. ∃k. a≠b ∧ a≠c ∧ b≠c ∧ kthia ∧ kthjb ∧ kthkc ∃a.∃b.∃c.∃i.∃j.∃k.a b ∧ a c ∧ b c ∧ kthia ∧ kthjb ∧ kthkc(1)
    Another phrasing would be
    ∃a. ∃b. ∃c. a≠b ∧ a≠c ∧ b≠c ∧ ∃k. kthka ∧ ∃k. kthkb ∧ ∃k. kthkc ∃a.∃b.∃c.a b ∧ a c ∧ b c ∧ ∃k. kthka ∧ ∃k. kthkb ∧ ∃k. kthkc (2)
    Observe that the trait "contains three unique numbers" does not mean "only contains three unique numbers" (though you could express that concept as well, if you like).
  3. The sequence is sorted ascending (with duplicates allowed) iff
    ∀a. ∀b. ∀i. ∀j. i≤j ∧ kthia ∧ kthjb → a≤b ∀a.∀b.∀i.∀j. i j ∧ kthia ∧ kthjb → a b(3)
    . This holds for both infinite and finite sequences, as long as kthkth models a sequence as described.
  4. We'll let zz represent the index of the one (possibly) out-of-order element, and just repeat the above formula but if either of the indices ii,jj is zz, then we don't require the ordering part to hold. This would almost work, but we also need to tack on a clause which allows the empty sequence (which certainly doesn't have more than one out-of-order element in it).
    ∃z. ∀a. ∀b. ∀i. ∀j. z=i ∨ z=j ∨ i<=j ∧ kthia ∧ kthjb → a<=b ∨ ¬ ∃n. ∃k. kthkn ∃z. ∀a. ∀b. ∀i. ∀j. z i ∨ z j ∨ <= i j ∧ kthia ∧ kthjb → <= a b ∨ ¬ ∃n. ∃k. kthkn (4)
    Another equivalent approach is to say "it is not the case, that there exist two out-of-order elements ii and jj". This is a bit unwieldy, because "ii is an out-of-order element" means "there exists kk which witnesses ii out of order, where kk isn't jj", and a witness can either be a larger or a smaller index (each case needing its own subformula).

Exercise 9

(7 pts) Alternation of quantifiers: Determine the truth of each of the following sentences in each of the indicated domains.

hint:

To help yourself, you might want to develop an English version of what the logic sentences say. Start with the inner formula (talking about people xx,yy,zz), then add the quantifier for zz to get a statement about people xx,yy, and repeat for the other two quantifiers.
  • S2: ∀x. ∀y. ∃z. likesxy ∧ z≠y → ¬likesyz∀x.∀y.∃z.likesxy ∧ z y → ¬likesyz
  • S3: ∃x. ∀y. ∀z. likesxy ∧ z≠y → ¬likesyz∃x.∀y.∀z.likesxy ∧ z y → ¬likesyz
  • S4: ∃x. ∃y. ∀z. likesxy ∧ z≠y → ¬likesyz∃x.∃y.∀z.likesxy ∧ z y → ¬likesyz
  • S5: ∀x. ∃y. ∀z. likesxy ∧ z≠y → ¬likesyz∀x.∃y.∀z.likesxy ∧ z y → ¬likesyz

  • D0: The empty domain.
  • D1: A world with one person, who doesn't like herself.
  • D2: A world with Yorick and Zelda, where Yorick likes Zelda, Zelda likes herself, and that's all.
  • D3: A world with many people, including CJ (Catherine Zeta-Jones), JC (John Cusack), and JR (Julia Roberts). Everybody likes themselves; everybody likes JC; everybody likes CJ except JR; everybody likes JR except CJ and IB. Any others may or may not like each other, as you choose, subject to the preceding. (You may wish to sketch a graph of this likeslikes relation.)
Note how we don't just specify the domain which the logic variables range over, but also how to interpret the logic's relation-symbol likeslikes.

Table 1: Determine the truth of these combinations.
\\D0D1D2D3
S2
S3
S4
S5

Solution

Note:
An incorrect solution was posted for a day -- "S2"..."S5" should have been relabeled "S5", "S2", "S3", "S4" (in effect, needing to rotating the table up a row). Fixed here.
Table 2: The truth of these combinations.
//D0D1D2D3
S2 truefalsefalsefalse
S3 falsefalsefalsefalse
S4 falsefalsetruefalse
S5 truefalsetruefalse

Here are English representations of these sentences.

  • S2: "Everybody likes everybody, and there's somebody all others dislike."
  • S3: "Somebody likes everybody, and everybody dislikes all others."
  • S4: "Somebody likes some person yy who dislikes all others."
  • S5: "Everybody likes some person yy who dislikes all others."

Reasoning with Equivalences

Exercise 10

(4pts) In class, we characterized a prime number as a number zz satisfying ∀q. ∀r. qr=z → q=1 ∨ r=1∀q.∀r.q r z → q 1 ∨ r 1 . Using the algebraic equivalences for first-order logic, show step-by-step that this is equivalent to the formula ¬ ∃q. ∃r. qr=z ∧ q≠1 ∧ r≠1 ¬ ∃q. ∃r. qr z ∧ q 1 ∧ r 1 .

Solution

Table 3
1¬ ∃q. ∃r. qr=z ∧ q≠1 ∧ r≠1 ¬ ∃q. ∃r. qr z ∧ q 1 ∧ r 1  
2≡∀q. ¬ ∃r. qr=z ∧ q≠1 ∧ r≠1 ≡∀q.¬ ∃r. qr z ∧ q 1 ∧ r 1 Complementation of ∃∃
3≡∀q. ∀r. ¬ qr=z ∧ q≠1 ∧ r≠1 ≡∀q.∀r.¬ qr z ∧ q 1 ∧ r 1 Complementation of ∃∃
4≡∀q. ∀r. ¬qr=z ∨ q=1 ∨ r=1≡∀q.∀r.¬qr z ∨ q 1 ∨ r 1 DeMorgan's Law (twice), expanding the ≠ (not-equals) shorthand
5≡∀q. ∀r. qr=z → q=1 ∨ r=1≡∀q.∀r.qr z → q 1 ∨ r 1 Definition of →

Exercise 11

(5pts) Simplify the following formula, so that the body of each quantifier contains only a single atomic formula involving that quantified variable. (Recall, an atomic formula is one with no connectives.) Provide reasoning for each step of your simplification.

∀x. ∀y. ∃z. Ax ∧ By → Cz∀x.∀y.∃z.Ax ∧ By → Cz

Solution

Basically, we just repeatedly apply distribution equivalences. In the following, there is some choices as to which formula to simplify next, but all choices lead to the same final answer.

Table 4
1∀x. ∀y. ∃z. Ax ∧ By → Cz∀x.∀y.∃z.Ax ∧ By → Cz  
2≡∀x. ∀y. Ax ∧ By → ∃z. Cz ≡∀x.∀y.Ax ∧ By → ∃z. Cz Distribution of ∃∃ over →
3≡∀x. ∃y. Ax ∧ By → ∃z. Cz ≡∀x.∃y. Ax ∧ By → ∃z. Cz Distribution of ∀∀ over →
4≡∃x. ∃y. Ax ∧ By → ∃z. Cz ≡∃x. ∃y. Ax ∧ By → ∃z. Cz Distribution of ∀∀ over →
5≡∃x. Ax ∧ ∃y. By → ∃z. Cz ≡∃x. Ax ∧ ∃y. By → ∃z. Cz Distribution of ∃∃ over ∧∧
6≡∃x. Ax ∧ ∃y. By → ∃z. Cz ≡∃x. Ax ∧ ∃y. By → ∃z. Cz Distribution of ∃∃ over ∧∧

One common mistake is as follows: ∀x. ∀y. Ax ∧ By → ∃z. Cz ≡ ∀x. ∀y. Ax ∧ By → ∃z. Cz ∀x.∀y.Ax ∧ By → ∃z. Cz ≡∀x.∀y. Ax ∧ By → ∃z. Cz . (Some students made this error harder to spot by simultaneously combining it with another step, distributing the ∀y.∀y. over the ∧∧.)

This step is not correct -- the rule for distributing ∀∀ over φ → ψφ → ψ (where ψψ doesn't contain yy free) requires negating the quantifier: ∀y.φ → ψ ≡ ∃y.φ → ψ∀y.φ → ψ≡∃y.φ → ψ The reason this is the rule is because φφ is a disguised negation: φ → ψ ≡ ¬φ ∨ ψφ → ψ≡¬φ ∨ ψ.

Reasoning with Inference Rules

Deferred:

These final three exercises will be deferred to hw04 (after we have discussed the first-order inference rules in lecture).

Exercise 12

(4pts) Using the inference rules, formally prove problem (2e).

Solution

We show that ∀x. Px → ¬Sx∀x. Rx → Sx∀x. Qx → Px ⊢ ∀x. Qx → ¬Rx∀x. Px → ¬Sx∀x. Rx → Sx∀x. Qx → Px ⊢ ∀x. Qx → ¬Rx. The general outline is to strip off the ∀∀s (leaving formulas that all happen to have the same variable xx, arbitrary in each). From there, a bunch of regular ol' inference rules, and a final ∀∀Intro to get our conclusion.

Table 5
1∀x. Px → ¬Sx∀x.Px → ¬Sx premise
2Px → ¬SxPx → ¬Sx ∀∀Elim line 1 (xx now arbitrary)
3∀x. Rx → Sx∀x.Rx → Sx premise
4Rx → SxRx → Sx ∀∀Elim line 3 (xx now arbitrary)
5∀x. Qx → Px∀x.Qx → Px premise
6Qx → PxQx → Px ∀∀Elim line 5 (xx now arbitrary)
7subproof:Qx ⊢ ¬RxQx ⊢ ¬Rx  
7.a  QxQxpremise
7.b  PxPx→→Elim, lines 7a, 6.
7.c  ¬Sx¬Sx→→Elim, lines 7b, 2.
7.d  ¬Sx → ¬Rx¬Sx → ¬RxTh'm: contrapositive (see below), line 4.
7.e  ¬Rx¬Rx→→Elim, lines 7d, 7c.
8Qx → ¬RxQx → ¬Rx →→Intro, line 7. (Note xx arbitrary.)
9∀x. Qx → ¬Rx∀x.Qx → ¬Rx ∀∀Intro, line 8 (since xx arbtrary).

Doing the above, we realized that we wanted to use the contrapositive in line 7d. We don't have φ → ψ ⊢ ¬ψ → ¬φφ → ψ ⊢ ¬ψ → ¬φ as one of our inference rules, but it's easy enough to do so:

Table 6
1φ → ψφ → ψ  premise
2subproof:¬ψ ⊢ ¬φ¬ψ ⊢ ¬φ   
2.a  ¬ψ¬ψ premise
2.b  subproof:φ ⊢ falseφ ⊢   
2.b.i   φφpremise
2.b.ii   ψψ→→Intro, lines 1, 2b.i.
2.b.iii   falsefalseIntro, lines 2b.ii, 2a.
2.c  ¬φ¬φ RAA', line 2b.
3¬ψ → ¬φ¬ψ → ¬φ  →→Intro, line 2.

Exercise 13

(3pts) What is wrong with the following "proof" of ∃x. Ex → Ec∃x. Ex → Ec?

Table 7
1subproof:∃x. Ex ⊢ Ec∃x. Ex ⊢ Ec  
1.a  ∃x. Ex∃x.Ex premise for subproof
1.b  EcEc ∃∃Elim, by line 1.1
2∃x. Ex → Ec∃x. Ex → Ec  →→Intro, by line 1

Solution

In line 1b, we cannot use ∃∃Elim to introduce the constant name cc, since cc occurs in the proof's conclusion. (This is explicitly against one of ∃∃Elim's caveats.)

First, to realize that this proof is indeed incorrect, consider the interpretation where the domain is integers, the EE is even?even?, and the free variable cc is interpreted as three. Clearly the conclusion is correct, since while there does exist an even integer, three is not even.

Until the final step, cc is an name for some unspecified constant -- one that is assumed to be even. But, by being left free in the conclusion, we are able to assign an interpretation that gives cc an inconsistent meaning.

Note that if we added one more ∃∃Intro step to the end of the proof, the resulting conclusion, ∃c. ∃x. Ex → Ec∃c.∃x. Ex → Ec , is indeed correct (if not terribly interesting). Here, cc is bound, and thus protected from gaining any undesired meaning from an interpretation.

Exercise 14

(6pts)

  1. (4pts)Prove the following: ∃x. Px ∀y. Py → Qy ⊢ ∃z. Qz ∃x. Px ∀y. Py → Qy ⊢ ∃z. Qz
  2. Give an interpretation in which these premises are true.
  3. Why shouldn't and can't we conclude ∀z. Qz∀z.Qz ?

Solution

Table 8
1∃x. Px∃x.Px premise
2PcPc ∃∃Elim, by line 1
3∀y. Py → Qy∀y.Py → Qy premise
4Pc → QcPc → Qc ∀∀Elim, by line 3, with tt=cc.
5QcQc →→Elim, by lines 2,4
6∃z. Qz∃z.Qz ∃∃Intro, by line 5

Note that in line 4, during ∀∀Elim we are allowed to replace yy with any term tt. We happened to choose the convenient term cc (a single variable). Another approach would have been to replace it with an arbitrary variable yy or ww or such, and then have one addiional re-naming step (where you can rename arbitrary variables at will).

  • One of many such interpretation consists of the domain of students, where PP is "gets an A grade", and QQ is "gets a passing grade". The premises are then that all students who get an A also pass, and that some student gets an A.
  • In the last step, we can't use ∀∀Intro, since cc was introduced by a use of ∃∃Elim (step 2) that this step depends on. Thus, we can't prove the conclusion with ∀∀ instead of ∃∃. Indeed, we shouldn't want the conclusion to hold in the ∀∀ version -- e.g. in the sample interpretation, it certainly isn't correct to conclude that all students pass (although I certainly hope that they do!).

Footnotes

  1. Dumas' original musketeers presumably meant something different -- that each one of them was for all; but this makes the sentence more boring for domains which include everybody, rather than just Athos, Porthos, and Aramis.) The English is meant to convey group unity -- so, the first part is trying to say "All for [the same] one particular person", rather than "each for their own one favorite." (Whew, natural language sure can be ambiguous! 'Course, that's one of its strengths, in non-engineering areas.)

Comments, questions, feedback, criticisms?

Send feedback