TAOCP 7.2.2.2 Exercise 2

Section 7.2.2.2: Satisfiability

Exercise 2. [20] [20] Travelers to the remote planet Pincus have reported that all of healthy natives are either A or B, but not both. Sane natives are happy, and many are healthy though hairless. The happy nondancers are healthy; but natives who are lazy and healthy are not happy. Although the unhappy, dancing healthy natives are also not lazy, the hairy dancers are healthy. What can we conclude from the unsane observed of native Pincus?

Verified: no
Solve time: 58s

Solution

Let the predicates for a native be $H$ for healthy, $S$ for sane, $P$ for happy, $D$ for dancing, $L$ for lazy, $Y$ for hairy, and let $A$ and $B$ denote the two exclusive healthy types.

The given statements can be written as

$$ H \to ((A\lor B)\land \neg(A\land B)), $$

$$ S\to P, $$

$$ P\land \neg D\to H, $$

$$ L\land H\to \neg P, $$

$$ \neg P\land D\land H\to \neg L, $$

$$ Y\land D\to H. $$

We are asked what follows from observing that a native is unsane, meaning that the native is not sane:

$$ \neg S. $$

The only statement involving $S$ is

$$ S\to P. $$

Its contrapositive is

$$ \neg P\to \neg S. $$

This implication says that an unhappy native must be unsane, but it does not give the converse implication. From $\neg S$ we cannot infer $\neg P$, because an unsane native may still be happy. The implication $S\to P$ permits both sane and unsane happy natives.

The remaining statements concern health, happiness, dancing, laziness, hairiness, and the alternatives $A$ and $B$. None of them has $\neg S$ as a hypothesis or conclusion. Therefore the observation $\neg S$ gives no further forced information about any of these properties.

Hence the only definite conclusion is that the native is not sane. No conclusion about health, happiness, dancing, laziness, hairiness, or membership in the classes $A$ and $B$ follows from the observation alone.

$$ \boxed{\text{An observed unsane native is not known to be healthy, happy, unhappy, lazy, or any other stated type.}} $$