All (non-practice, non-extra-credit) problems
due 2004.Feb.03 (Tue) 17:00.
Rice Students: If you like, you can play WaterWorld
on OwlNet, in /home/comp280/bin/waterworld.
To run Waterworld on your home computer,
download (from owlnet) the directory
/home/scheme/plt/205/collects/waterworld/,
and (from drscheme) add it as a teachpack.
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, χ ∨ υ ⊢ υ ∨ χχ ∨ υ ⊢ υ ∨ χ.
Table 1
| 1 | χ ∨ υχ ∨ υ | | premise
|
| 2 | subproof:χ ⊢ υ ∨ χχ ⊢ υ ∨ χ | | |
| 2.a | | χχ | premise for subproof
|
| 2.b | | υ ∨ χυ ∨ χ | ∨∨Intro
|
| 3 | subproof:υ ⊢ υ ∨ χυ ⊢ υ ∨ χ | | |
| 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 ∧∧.
Table 2
| 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
¬¬χ ∧ υ ⊢ false¬¬χ ∧ υ ⊢ .
(That is, the rule's φφ refers to a WFF which is already a negation:
"¬χ ∧ υ¬χ ∧ υ". Not a problem at all.)
Table 3
| 1 | ¬χ¬χ | | premise
|
| 2 | subproof:¬¬χ ∧ υ ⊢ false¬¬χ ∧ υ ⊢ | | |
| 2.a | | ¬¬χ ∧ υ¬¬χ ∧ υ | premise for subproof
|
| 2.b | | χ ∧ υχ ∧ υ | ¬¬Elim,
by line 2.1
|
| 2.c | | χχ | ∧∧Elim,
by line 2.2
|
| 2.d | | false | falseIntro,
by lines 1,2.3
|
| 3 | ¬χ ∧ υ¬χ ∧ υ | | RAA,
by line 2,
where φφ=¬χ ∧ υ¬χ ∧ υ
|
(6pts.)
Show that
¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe¬W-safe ∨ ¬Y-unsafe ⊢ W-unsafe ∨ Y-safe.
Use the ∨∨Elim inference rule to get the final result.
Table 4
| 1 | ¬W-safe ∨ ¬Y-unsafe¬W-safe ∨ ¬Y-unsafe | | premise
|
| 2 | subproof:¬W-safe ⊢ W-unsafe ∨ Y-safe¬W-safe ⊢ W-unsafe ∨ Y-safe | | |
| 2.a | | ¬W-safe¬W-safe | premise for subproof
|
| 2.b | | ¬W-safe → W-unsafe¬W-safe → W-unsafe | WaterWorld domain axiom
|
| 2.c | | W-unsafeW-unsafe | →→Elim
|
| 2.d | | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | ∨∨Intro
|
| 3 | subproof:¬Y-unsafe ⊢ W-unsafe ∨ Y-safe¬Y-unsafe ⊢ W-unsafe ∨ Y-safe | | |
| 3.a | | ¬Y-unsafe¬Y-unsafe | premise for subproof
|
| 3.b | | ¬Y-unsafe → Y-safe¬Y-unsafe → Y-safe | WaterWorld domain axiom
|
| 3.c | | Y-safeY-safe | →→Elim
|
| 3.d | | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | ∨∨Intro
|
| 4 | W-unsafe ∨ Y-safeW-unsafe ∨ Y-safe | | ∨∨Elim
|
(5pts)
For the following WaterWorld proof of
X-has-1 ⊢ W-unsafe ∨ Y-unsafeX-has-1 ⊢ W-unsafe ∨ Y-unsafe,
provide the missing steps and/or reasons:
Table 5
| 1 | X-has-1X-has-1 | | ____________
|
| 2 | ____________ | | WaterWorld domain axiom
|
| 3 | ____________ | | →→Elim
|
| 4 | subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafeW-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 4.a | | W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe | premise for subproof
|
| 4.b | | Y-unsafeY-unsafe | ____________
|
| 4.c | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ____________
|
| 5 | subproof:¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 5.a | | ¬W-safe ∧ Y-unsafe¬W-safe ∧ Y-unsafe | premise for subproof
|
| 5.b | | W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe | CaseElim (left),
where φφ=____________,
and ψψ=____________.
|
| 5.c | | ____________ | ____________
|
| 5.d | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ____________
|
| 6 | W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafe | | From class, φ ∨ ¬φφ ∨ ¬φ,
with φ____________φ____________
|
| 7 | W-unsafe ∨ Y-unsafeW-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) φ ∨ ¬φφ ∨ ¬φ.
Table 6
| 1 | X-has-1X-has-1 | | premise
|
| 2 | X-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeX-has-1 → W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe | | WaterWorld domain axiom
|
| 3 | W-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safeW-safe ∧ Y-unsafe ∨ W-unsafe ∧ Y-safe | | →→Elim
|
| 4 | subproof:W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafeW-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 4.a | | W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe | premise for subproof
|
| 4.b | | Y-unsafeY-unsafe | ∧∧Elim
|
| 4.c | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ∨∨Intro
|
| 5 | subproof:¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe¬W-safe ∧ Y-unsafe ⊢ W-unsafe ∨ Y-unsafe | | |
| 5.a | | ¬W-safe ∧ Y-unsafe¬W-safe ∧ Y-unsafe | premise for subproof
|
| 5.b | | W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe | CaseElim (left),
where φφ=W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe,
and ψψ=W-unsafe ∧ Y-safeW-unsafe ∧ Y-safe
|
| 5.c | | W-unsafeW-unsafe | ∧∧Elim
|
| 5.d | | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | ∨∨Intro
|
| 6 | W-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafeW-safe ∧ Y-unsafe ∨ ¬W-safe ∧ Y-unsafe | | From class, φ ∨ ¬φφ ∨ ¬φ,
with φW-safe ∧ Y-unsafeφW-safe ∧ Y-unsafe
|
| 7 | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | | ∨∨Elim,
by lines 5,6, with
φW-safe ∧ Y-unsafe
ψ¬W-safe ∧ Y-unsafe
θW-unsafe ∨ Y-unsafeφW-safe ∧ Y-unsafeψ¬W-safe ∧ Y-unsafeθW-unsafe ∨ Y-unsafe
|
[practice; 0pts]
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-safeQ-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe.
- Not only is Y-safeY-safe an allowable premise
(reading off the given board),
but so is ¬Y-unsafe¬Y-unsafe.
Table 7
| 1 | Q-has-1Q-has-1 | | premise
|
| 2 | X-has-1X-has-1 | | premise
|
| 3 | ¬Y-unsafe¬Y-unsafe | | premise
|
| 4 | X-has-1 → Y-unsafe ∨ W-unsafeX-has-1 → Y-unsafe ∨ W-unsafe | | th'm: previous problem (and, →→Intro)
|
| 5 | W-unsafe ∨ Y-unsafeW-unsafe ∨ Y-unsafe | | →→Elim,
by lines 2,4
|
| 6 | Y-unsafe ∨ W-unsafeY-unsafe ∨ W-unsafe | | ∨∨ commutes; line 5
|
| 7 | W-unsafeW-unsafe | | CaseElim,
by lines 3,6
|
| 8 | subproof:¬¬P-safe ∧ W-safe ⊢ false¬¬P-safe ∧ W-safe ⊢ | | |
| 8.a | | ¬¬P-safe ∧ W-safe¬¬P-safe ∧ W-safe | premise for subproof
|
| 8.b | | P-safe ∧ W-safeP-safe ∧ W-safe | ¬¬Elim,
by line 8.1
|
| 8.c | | W-safeW-safe | ∧∧Elim
|
| 8.d | | W-safe → ¬W-unsafeW-safe → ¬W-unsafe | WaterWorld domain axiom
|
| 8.e | | ¬W-unsafe¬W-unsafe | →→Elim,
by lines 8.2,8.3
|
| 8.f | | false | falseIntro,
by lines 7,8.4
|
| 9 | ¬P-safe ∧ W-safe¬P-safe ∧ W-safe | | RAA,
by line 8
|
| 10 | subproof:¬¬R-safe ∧ W-safe ⊢ false¬¬R-safe ∧ W-safe ⊢ | | |
| 10.a | | ¬¬R-safe ∧ W-safe¬¬R-safe ∧ W-safe | premise for subproof
|
| 10.b | | R-safe ∧ W-safeR-safe ∧ W-safe | ¬¬Elim,
by line 10.1
|
| 10.c | | W-safeW-safe | ∧∧Elim
|
| 10.d | | W-safe → ¬W-unsafeW-safe → ¬W-unsafe | WaterWorld domain axiom
|
| 10.e | | ¬W-unsafe¬W-unsafe | →→Elim,
by lines 10.2,10.3
|
| 10.f | | false | falseIntro,
by lines 7,10.4
|
| 11 | ¬R-safe ∧ W-safe¬R-safe ∧ W-safe | | RAA,
by line 10
|
| 12 | Q-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safeQ-has-1 → P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe | | Allowed by problem statement
|
| 13 | P-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safeP-safe ∧ R-safe ∨ P-safe ∧ W-safe ∨ R-safe ∧ W-safe | | →→Elim,
by lines 1,12
|
| 14 | R-safe ∧ W-safe ∨ P-safe ∧ R-safe ∨ P-safe ∧ W-safeR-safe ∧ W-safe ∨ P-safe ∧ R-safe ∨ P-safe ∧ W-safe | | ∨∨ commutes (ex.1),
by line 13
|
| 15 | P-safe ∧ R-safe ∨ P-safe ∧ W-safeP-safe ∧ R-safe ∨ P-safe ∧ W-safe | | CaseElim,
by lines 9,14
|
| 16 | P-safe ∧ W-safe ∨ P-safe ∧ R-safeP-safe ∧ W-safe ∨ P-safe ∧ R-safe | | Theorem: ∨∨ commutes (ex.1), line 15.
|
| 17 | P-safe ∧ R-safeP-safe ∧ R-safe | | CaseElim,
by lines 11,16.
|
| 18 | P-safeP-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-safeR-safe as a premise.
(In fact, we nearly proved that
¬R-safe¬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-1P-has-1 ∧ U-has-1 ∧ W-has-1,
but X-safeX-safe.
-
Compare this with
a previous theorem (example 11)
B-has-1 ∧ G-has-1 ∧ J-has-1 → K-unsafeB-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¬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),
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-1P-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-safeH-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-unsafeN-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-1totCount-is-1, totCount-is-2totCount-is-2, ….
(Indeed, you may have noticed that list of domain axioms makes
only a paltry attempt at including domain axioms involving
totCount-is-5totCount-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.)
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-safeZ-safe.
Observe that the proposition totCount-is-1totCount-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.)
(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 aa,bb in the domain,
atLeastAsWiseAsab ∨ atLeastAsWiseAsbaatLeastAsWiseAsab ∨ atLeastAsWiseAsba
-
For arbitrary aa in the domain,
primea → odda → primeaprimea → odda → primea
-
For arbitrary aa,bb in the domain,
betterThanab → ¬betterThanbabetterThanab → ¬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 ∨ atLeastAsWiseAsbaatLeastAsWiseAsab ∨ atLeastAsWiseAsba
is false when
the domain is {appleapple} and the relation
atLeastAsWiseAsatLeastAsWiseAs = {}.
However it is true for the same domain but interpreting
atLeastAsWiseAsatLeastAsWiseAs
= {apple appleapple apple}.
- Valid.
Choose any interpretation you like, and we'll show
that
primea → odda → primeaprimea → odda → primea
is true.
Let PP be the truth value
of primeaprimea
under that interpretation, and similarly
and let QQ be the truth value of
oddaodda.
Then (for that interpretation) the original formula
has the truth value
P → Q → PP → 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 → ¬betterThanbabetterThanab → ¬betterThanba
is false when the domain is {appleapple} and
betterThanbetterThan is interpreted
as {apple appleapple apple}.
This formula is true when the domain is the empty relation {}.
(In general, it is true whenever
betterThanbetterThan is interpeted
as a antisymmetric relation which is nowhere reflexive.)
Table 8: Truth-table for propositional analog of a relational formula.
| PP | QQ | P → Q → PP → Q → P |
| false | false | true |
| false | true | true |
| true | false | true |
| true | true | true |
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.)
(2 pts.) Rosen, Section 1.3, pg.40, #6.
Give English translations of the following, where
the domain is the students in your school, and
N
is the relation "has visited North Dakota".
- ∃x. Nx∃x.Nx
- ∀x. Nx∀x.Nx
- ¬∃x. Nx ¬∃x. Nx
- ∃x. ¬Nx∃x.¬Nx
- ¬∀x. Nx¬∀x. Nx
- ∀x. ¬Nx∀x.¬Nx
- ∃x. Nx∃x.Nx :
Some student in my school has visited North Dakota.
- ∀x. Nx∀x.Nx:
All students in my school have visited North Dakota.
- ¬∃x. Nx ¬∃x. Nx :
No student in my school has visited North Dakota.
- ∃x. ¬Nx∃x.¬Nx :
Some student in my school has not visited North Dakota.
- ¬∀x. Nx¬∀x. Nx:
Not all students in my school have visited North Dakota.
- ∀x. ¬Nx∀x.¬Nx:
All students in my school have not visited North Dakota.
(3 pts.) Rosen, Section 1.3, pg.40, #10.
- A student in your class has a cat, a dog, and a ferret.
- All students in your class have a cat, a dog, or a ferret.
- Some student in your class has a cat and a ferret but not a dog.
- No student in your class has a cat, a dog, and a ferret.
- For each of the three animals, there is a student in your class that has one.
- ∃x. Cx ∧ Dx ∧ Fx∃x.Cx ∧ Dx ∧ Fx
- ∀x. Cx ∨ Dx ∨ Fx∀x.Cx ∨ Dx ∨ Fx
- ∃x. Cx ∧ Fx ∧ ¬Dx∃x.Cx ∧ Fx ∧ ¬Dx
- ¬∃x. Cx ∧ Dx ∧ Fx ¬∃x. Cx ∧ Dx ∧ Fx
- ∃x. Cx ∧ ∃y. Dy ∧ ∃z. Fz∃x. Cx ∧ ∃y. Dy ∧ ∃z. Fz
(3 pts.) Rosen, Section 1.3, pg.41, #16.
- ∃x. x2=2∃x.=x 2 2
- ∃x. x2=-1∃x.=x 2 -1
- ∀x.
x2+2≥1∀x.
x 2
2
1
-
∀x.
x2≠x∀x.
x 2
x
- true (as witnessed by each of {-sqrt(2), sqrt(2)}).
- false.
- true.
- false (as witness by each of {0,1}).