x
White(x), Elephant(x) -> WhiteElephant(x)
x WhiteElephant(x)
-> White(x), Elephant(x)Part A
Ch.4 Q.15a) There are several ways to express these, depending on whether you make White(x) and Elephant(x) separate predicates, or have a predicate WhiteElephant(x). Since the statements never split the two, it's simpler to go with WhiteElephant(x). If anyone wants to quibble, we can always state as a preliminary:
Or, equivalently, we could use equivalence:
With that out of the way...WhiteElephant(x)
i) 
x WhiteElephant(x)
ii)
x WhiteElephant(x) ^ [
y WhiteElephant(y) -> Equals(x,y) ]
That is, if there's "another" white elephant, it's the same as x.iii)
x y
WhiteElephant(x) ^ WhiteElephant(y) ^ ~Equals(x,y)
That is, there are two different items x and y which are white elephants.iv)
x y
WhiteElephant(x) ^ WhiteElephant(y) ^ ~Equals(x,y)
^ [ z
WhiteElephant(z) -> ( Equals(x,z) v Equals(y,z)
) ]
First assert there are two distinct white elephants, then say that any "other" white elephant must be one of these.
Ch.4 Q.17) Again, there are several ways to express
these. For instance, if we choose a restricted domain, like "birds"
for a or "mountains" for b, then we don't need a predicate that tests whether
our variables are birds or mountains. I'll show one of each.
a)
x in {all things} ~( Bird(x) ^ Name(x, Tweety)
^ InWPZ(x) )
Why not just ~( Bird(Tweety) ^ InWPZ(Tweety) )? That's because there might be more than one bird named Tweety.b) Define Taller(r,s) to mean r is taller than s. Mt. Everest and Mt. Rainier are constants.
Could also push the ~ inside using DeMorgan's law. And it would also be fine to say:
x in {all
mountains on Earth} ~Taller(x, Mt. Everest)
y in {all
mountains on Earth} InWashington(y) ^ (~Taller(y, Mt. Rainier) )
The above expressions say there is no mountain taller than Mt. Everest, and there is no mountain in Washington taller than Mt. Rainier. The two expressions are independent.c) We could define function names like exp(x,n) = xn and sum(x,y) = x + y, or, more formally, use single-letter names...or we could stick with the non-standard but more meaningful original forms. Either is ok -- I'll do the latter. I'd rather just use = and <= for the predicates, too.
Let N = positive integers and I = all integers. Let LE(r,s) mean r <= s. Equals is as usual.
x, y,
z in I,
n in N Equals( xn + yn, zn
) -> LE(n, 2)
This says that if xn + yn = zn, then n must be <= 2.
Ch.6 Q.15)
P1:
x HasHair(x) ^ GivesMilk(x) -> IsMammal(x)
P2:
x Coconut(x) -> HasHair(x)
P3:
x Coconut(x) -> GivesMilk(x)
P4:
x Coconut(x) -> IsMammal(x)
Show P4 from P1, P2, P3 using resolution. First put these in clause form. Eliminate -> and make the variables unique (but we're going to undo that in a moment...)
P1:
x ~( HasHair(x) ^ GivesMilk(x) ) v IsMammal(x)
P1:
x ~HasHair(x) v ~GivesMilk(x) v IsMammal(x)
P2:
y ~Coconut(y) v HasHair(y)
P3:
z ~Coconut(z) v GivesMilk(z)
P4:
w ~Coconut(w) v IsMammal(w)
P4 is the desired conclusion -- negate it because we're going to try to show a contradiction. The negated universal quantifier becomes an existential quantifier with its expression negated. Use DeMorgan's to distribute the resulting negation. Call the new statement N.
N: ~( w
~Coconut(w) v IsMammal(w) )
N:
w ~( ~Coconut(w) v IsMammal(w) ) )
N:
w Coconut(w) ^ ~IsMammal(w)
Get rid of the existential quantifier by Skolemization -- give a constant name to the instance for which the statement must be true:
N: Coconut(a) ^ ~IsMammal(a)
Split N into its two clauses.
Na: Coconut(a)
Nb: ~IsMammal(a)
Drop the universal quantifiers in P1-3 -- we'll assume that for all variables.
P1: ~HasHair(x) v ~GivesMilk(x) v IsMammal(x)
P2: ~Coconut(y) v HasHair(y)
P3: ~Coconut(z) v GivesMilk(z)
Recall we're taking these all to be true at once. We have some pairs we could use resolution on, but first we need to unify their arguments. Unify P2 and Na by substituting a for y. Likewise unify P3 and Na by substituting a for z. (We can't substitute a variable for a constant -- that would broaden the interpretation -- but we can narrow the scopy by substituting a constant for a variable.)
P2: ~Coconut(a) v HasHair(a)
P3: ~Coconut(a) v GivesMilk(a)
Na: Coconut(a)
Apply resolution:
P2': HasHair(a)
P3': GivesMilk(a)
Note that P1 can be resolved with these one at a time, but first substitute a in for x:
P1: ~HasHair(a) v ~GivesMilk(a) v IsMammal(a)
Resolve P2' and P1:
P2'': ~GivesMilk(a) v IsMammal(a)
Resolve P3' and P2'':
P3'': IsMammal(a)
Resolve P3'': IsMammal(a), and Nb: ~IsMammal(a), to get nothing:
N': empty
So we've shown that combining the contradiction of P4 with P1-3 leads to failure -> P4 is true.
-- Pat