Review
In a previous post we began examining the Three Hats Puzzle. Here we complete our solution. So far, we've introduced axioms characterizing a domain of five hats (two blue and three red) and three individuals (Alex, Barbara, and Cherise). We've additionally asserted that Alex and Barbara may see the hats of other participants, but Cherise cannot, and that neither Alex nor Barbara know what color hat they are wearing, while Cherise knows her hat color. From these axioms we were able to infer if Alex (or Barbara) sees two hats, then they cannot both be blue. This should sound correct, since if, say, Alex saw two blue hats, and since there are only two blue hats, then Alex would know his hat color. Since he doesn't, he doesn't.
To solve the puzzle, however, we must infer that Cherise knows her hat color.
Informal Solution
We will ultimately introduce first-order axioms and infer the solution to the case, but first we should examine the case informally to see what axioms we might need. Let's think about Alex for a moment.
- We know Alex may see two red hats. To see why, note that if Alex sees two red hats, then he does not know what color hat he is wearing, i.e. he could be wearing a blue hat or red hat. Moreover, Barbara gains no new information based on Alex's claim that he does now know what color hat he is wearing, as all three participants could be wearing red hats.
- We know Alex may see a red hat and a blue hat, but here we must be careful. The distribution of the hats matters. It is permissible for Alex to see Barbara wearing a blue hat and Cherise wearing a red hat. Then Alex's hat may be blue or red. Moreover, Barbara gains little information from Alex's claim. If Alex's hat is, say, red and Cherise's hat is red, then Barbara's hat may be red or blue.
- Note, however, Alex cannot see Barbara wearing a red hat and Cherise wearing a blue hat. This leads to contradiction. To see why, assume Cherise is wearing a blue hat. Then both Alex and Barbara see Cherise wearing a blue hat. Alex may speak truly when claiming he does not know what color hat he is wearing, as he may see Barbara wearing a red hat and Cherise wearing a blue hat. Nevertheless, this option leaves Barbara speaking falsely. For if Barbara sees Cherise wearing a blue hat and knows that Alex cannot see two blue hats and also knows that Alex does not know what color hat he is wearing, then Barbara can infer that her hat must be red. Clearly, if Barbara's hat were blue then Alex would know what color hat he's wearing, as there are only two blue hats.
Our informal solution results in only two options for Alex. Alex either sees two red hats or Barbara wearing a blue hat and Cherise wearing a red hat.
More importantly than all that though, is the fact that we've stumbled upon our solution to the problem! On either of these options it must be the case that Cherise is wearing a red hat. Indeed, this is information Cherise may infer from the constraints of the case. In other words, Cherise knows what color hat she is wearing without being able to see any hats at all.
Strengthening our Axioms
Our only task remaining is to formalize our informal solution, and verify the intended results follow from our formalization. To our axiom set we add the binary relation "W" with an intended reading that the first (individual) wears the second (hat).
1. ∀x∀y∀z((W(x,z) & W(y,z)) -> x=y)
Only one individual may wear a given hat
2. ∀x∀y∀z((W(x,y) & W(x,z)) -> y=z)
Every individual wears only one hat
3. ∀x∀y(W(x,y) -> (I(x) & H(y)))
Only individuals wear hats
We also require that seeing a hat entails the hat is being worn, but no one sees the hat they are wearing.
4. ∀x∀y(S(x,y) -> ∃z(W(z,y)))
If someone sees a hat then it's being worn by someone
5. ~(∃x∃y(S(x,y) & W(x,y)))
No one sees the hat they are wearing
Supplementing these general axioms are the following facts, reflecting that, say, anything Alex sees is either Barbara's or Cherise's hat (and mutatis mutandis for Barbara).
6. ∀x(S(a,x) -> (W(b,x) v W(c,x)))
Alex sees the hats Barbara and Cherise wear
7. ∀x(S(b,x) -> (W(a,x) v W(c,x)))
Barbara sees the hats Alex and Cherise wear
Finally, we add the fact that if Barbara sees Cherise wearing a blue hat, then Barbara knows what color hat she is wearing.
8. ∀x((S(b,x) & W(c,x) & B(x)) -> K(b,b))
If Barbara sees Cherise wearing a blue hat, Barbara knows what color hat she is wearing
These axioms and facts generate a class of models in which the following are permissible:
9. ∃x∃y(S(a,x) & S(a,y) & x≠y & R(x) & R(y))
Alex sees two red hats
10. ∃x∃y(S(b,x) & S(b,y) & x≠y & R(x) & R(y))
Barbara sees two red hats
11. ∃x∃y(S(a,x) & S(a,y) & x≠y & B(x) & R(y) & W(b,x) & W(c,y))
Alex sees Barbara wearing a blue and Cherise wearing a red hat
But, importantly, which rule out the following possibilities:
12. ∃x∃y(S(a,x) & S(a,y) & x≠y & R(x) & B(y) & W(b,x) & W(c,y))
Alex sees Barbara wearing a red hat and Cherise wearing a blue hat
13. ∃x(S(a,x) & B(x) & W(c,x))
Alex sees Cherise wearing a blue hat
Hence, we are able to infer that Cherise is wearing a red hat, i.e. the following is a theorem:
14. ∃x(W(c,x) & R(x))
Cherise is wearing a red hat
Which is essentially what we intended to show. The resulting axiom set thus far can be found here. (Exercise: Show Cherise knows the color of her own hat).
Checking Our Work
Proofs were generated with Prover9 and models were checked with Mace4. If you'd like to check the models yourself, I advise generating a model with Mace4, then looking at the 'cooked version'. You can make the model even more perspicuous by copying it into Notepad++, hitting ctrl+F, navigating to the "Mark" tab, then entering "-*" (no quotes) with "Bookmark Line" selected. This will bookmark each line that begins with "-" which, in Mace4 means the predicate or relation is not satisfied. You can then navigate to Search->Bookmark->Remove Bookmarked Lines, to remove all the unsatisfied predicates and relations. The result will be a small model that's easy to read.