1 Blue Eyes
Lost somewhere in the vastness of the ocean, a group of logicians find themselves stranded on a deserted island. One hundred of these logicians have blue eyes, another hundred have brown eyes, and a single character–the guru–has green eyes. The only way off the island is a ship that arrives each night. However, to leave with the ship, an islander must know the color of their own eyes. Unfortunately, with no mirrors, and nothing reflective, nobody can independently determine the color of their own eyes. That is, until the guru makes a proclamation: “I see a person with blue eyes.” Who leaves the island?
This is the Blue Eyes logic puzzle, as formulated by the author behind xkcd. The starting clue we get is this: somebody leaves the island, however improbable it seems after a quick consideration. So who?
To answer that question, we’ll work through some examples and a proof, and finish by modeling the island in TLA+.
2 First Steps
The first thing that stands out is the numbers picked–having exactly 100 blue-eyed people and 100 brown-eyed people feels pretty arbitrary. Let’s break the problem into smaller cases, and see if that gives a better picture of what’s going on.
Case 1
Let’s consider the case where the island has only 3 people: one person with blue eyes, one with brown, and the guru with green eyes. Consider what each person sees:
| Visible to Observer
| |||
| Observer | blue | brown | green |
| blue | 0 | 1 | 1 |
| brown | 1 | 0 | 1 |
| green | 1 | 1 | 0 |
As soon as the guru says “I see a person with blue eyes,” the one blue-eyed person can look around, observe that nobody they see has blue eyes, and conclude immediately that it must be them. They leave the first night.
Note how this looks from the perspective of the one brown-eyed person: they can see the same blue-eyed person the guru sees, but not their own eye color–so they don’t know if the guru is referring to them, or to the blue-eyed person they see!
Case 2
Let’s expand the island to contain 5 people: 2 blue, 2 brown, and 1 green. Here’s an updated summary of what each person sees:
| Visible to Observer
| |||
| Observer | blue | brown | green |
| blue | 1 | 2 | 1 |
| brown | 2 | 1 | 1 |
| green | 2 | 2 | 0 |
Oh no! This is now an ambiguous situation for everybody. Previously, the blue-eyed person knew immediately that they could leave, and only green and brown were unsure. Now everybody is uncertain and has no choice but to stay on the island.
However, consider the scene on the morning of the second day: everybody wakes up, looks around, and sees that nobody left last night. Being perfect logicians, this brings good news for all of the blue-eyed people. Why?
Both blue-eyed people see one blue-eyed person, but don’t know if the person the guru is talking about is the person they see, or themselves. Since the blue-eyed person didn’t leave, this lets them deduce a really valuable piece of information: the blue-eyed person that they see sees somebody else with blue-eyes!
Following the same process of elimination as before, all ambiguity is removed for both blue-eyed people, and both of them leave the island on the second night.
3 Proving What We Know
The structure of these two cases suggests a proof by induction. We know what happens on the island as more blue- and brown-eyed people are added.
One observation that will help structure the proof is that it’s each day that passes that brings extra information. So, we’ll do a proof by induction on the number of days since the guru’s proclamation.
Now, what do we want to prove? Key to the above two cases was establishing a lower bound on the number of blue-eyed people. This allowed all blue-eyed people to use the pigeonhole principle to deduce that they must have blue eyes.
To establish that lower bound, we’ll prove that (no. of blue-eyed people) > (no. of days since announcement), as long as there are blue-eyed people on the island.
Proof, by induction on days, where days is the number of days since the guru’s announcement and blue is a lower-bound on the number of blue-eyed people on the island known to all islanders.
Show that for all days ≥ 0, (∃ person | eye color is blue)
blue > days.
Base Case
Sp days = 0.
By proclamation of the guru on day 0, ∃ person | eye color is blue, so blue ≥ 1 and blue > days.
∴ the inductive hypothesis (∃ person | eye color is blue)
blue > days holds for days = 0.
Inductive Case
Sp days = N, for some N ≥ 0, and (∃ person | eye color is blue)
blue > N.
(Show blue > N + 1 on day N + 1)
Consider the next day, day N + 1.
Sp (∃ person | eye color is blue) on day N + 1.
Sp there are N + 1 blue-eyed people, satisfying blue > N
All blue-eyed people see N blue-eyed people.
By the pigeonhole principle, on previous day N, knowing that blue > N and seeing only N blue-eyed people, all blue-eyed people may deduce that they have blue eyes and leave the island.
However, all blue-eyed people did not leave the island.
By contradiction, there are more than N + 1 blue-eyed people, and blue≠N + 1.
Since blue > N and blue≠N + 1, blue > N + 1.
∴ on day N +1, (∃ person | eye color is blue)
blue > days.
On the other hand, Sp ¬(∃ person | eye color is blue) on day N + 1.
(∃ person | eye color is blue)
blue > days is true by definition of implies.
∴ by division into cases, (∃ person | eye color is blue)
blue > days holds for day N + 1.
Therefore, by induction on days, (∃ person | eye color is blue)
blue > days holds for all days ≥ 0.
□
4 Application to Our Island
In the case of our specific island, there are 100 blue-eyed people, 100 brown-eyed people, and the guru. Let’s use the proof above to show that on an island with N blue-eyed people, all blue-eyed people leave on day N − 1.
Proof, using days and blue as defined previously.
Consider an island with the following population: N blue-eyed residents, M brown-eyed residents, and a green-eyed guru, where N ≥ 2 and M ≥ 2.
Since each individual cannot see their own eyes, each islander sees the following:
Observer blue brown green blue N − 1 M 1 brown N M − 1 1 green N M 0 Consider the days 0 through N − 2.
By the previous proof, the best lower bound that can be established for blue is blue > N − 2. N − 1 is the smallest value that satisfies this inequality, but since each blue-eyed person sees N −1 blue-eyed people, they can’t deduce that they have blue eyes and must remain on the island.
Consider the day N − 1.
Since no blue-eyed people could leave for days 0 through N − 2, on day N − 1, ∃ person | eye color is blue.
By the previous proof, this implies that blue > N − 1.
By the pigeonhole principle, since each blue-eyed person sees N −1 blue-eyed people and knows that blue > N −1, each blue-eyed person may conclude that they have blue eyes and leave the island at the end of day N − 1, or the Nth day.
All brown-eyed people and the guru see N blue-eyed people, so they cannot make this deduction and must remain on the island.
□
Applied to our island, we may conclude that with 100 blue-eyed people, all blue-eyed people leave on the 100th day.
5 What Next?
Following the structure of the above proofs, we can model the island as described using TLA+. I find that translating these proofs to TLA+ helps me to wrap my head around the problem and brings to light anything that was missed in the proof. It also allows us to follow the induction step-by-step and to examine state at each day.
The following TLA+ source didn’t translate 100% to HTML, so you can also follow along with the plain source here.
Here’s the module header and the constant expressions we’ll work with:
______________________________ module BlueEyes _____________________________
extends Naturals
variables days_passed, population, knowledge, lower_bound
All eye colors present on the island
Colors
{“blue”, “brown”, “green”}
The eye color observed by the guru
Observed
“blue”
record mapping eye color to population
InitialPopulation
[blue
100, brown
100, green
1]
The knowledge variable stores knowledge private to each eye color group. It records what a person of each eye color sees when they observe the island.
It’s initialized like this:
produce a record mapping eye color to local group knowledge
LookAround
[c ∈ Colors
visible is a modified Population record,
showing how many people of each eye color are visible to people with eye color c
[visible
[population except ![c] = (@ − 1)]]
]
The Init and Next state formulas below control how variables are initialized and how they may change.
Init
∧ days_passed = 0
∧ population = InitialPopulation
∧ knowledge = LookAround
Given globally available information,
how many people of each eye color can be deduced to be on the island?
∧ lower_bound = [c ∈ Colors
0]
Next
∨ GuruObservation
∨ ∧ Observe
∧ LeaveIsland
∧ NextDay
In Init, the lower_bound variable is initialized to zero for all eye colors. This models the situation where, before the guru makes their proclamation, there’s no global lower bound that can be agreed on by everybody on the island.
Looking at the next state formula, we can see there’s two top-level options: either the guru can make an observation, or we can work through one day by observing who’s on the island, leaving the island if eye color is known, and then moving on to the next day.
The GuruObservation formula looks like this:
On day zero, the guru observes one person with blue eyes.
Update the shared knowledge.
GuruObservation
∧ days_passed = 0
∧ lower_bound′ = [lower_bound except ![Observed] = 1]
∧ unchanged ⟨days_passed, population, knowledge⟩
Note that it’s only enabled on the first day. When activated, it updates the global knowledge appropriately, establishing a lower bound on how many blue-eyed people are on the island.
The Observe, LeaveIsland, and NextDay formulas update state after the guru’s proclamation.
Update individual and shared knowledge at the start of the day,
only if the guru has already made their observation
Observe
∧∃c ∈ domain lower_bound : lower_bound[c] > 0
∧ knowledge′ = LookAround
If one night passed and everybody with eye color Observed is still on the island,
there must be at least one more than originally deduced
∧ lower_bound′ = [lower_bound except ![Observed] = if population[Observed] > 0 then @ + 1 else @]
For a person of eye color c, if lower_bound > visible,
this person must have eye color c, and may leave the island
LeaveIsland
population′ = [c ∈ Colors
if lower_bound[c] > knowledge[c].visible[c]
then 0
else population[c]
]
Update state after the guru has made their observation
NextDay
∧ days_passed′ = days_passed + 1
The Observe step updates local and global knowledge only if the guru has made their proclamation. Next, the LeaveIsland forumula checks the updated knowledge and lower_bound variables to see if any group is able to leave the island and updates population accordingly.
With these forumals defined, it’s possible to plug Init and Next into the TLC model checker and let it run. However, it will run indefinitely, since we haven’t given it anything to check.
To get a useful result, we’ll define the PopulationInvariant formula, which asserts that population never changes, i.e. that no one leaves the island.
PopulationInvariant
population = InitialPopulation
Additionaly, we’ll create a TypeInvariant formula to make sure that the state variables have the expected type.
Type invariants for each state variable
TypeInvariant
∧ days_passed ∈ Nat
∧ ∧ domain population = Colors
∧∀c ∈ domain population : population[c] ∈ Nat
∧ ∧ domain knowledge = Colors
∧∀c ∈ domain knowledge :
∧ domain knowledge[c] = {“visible”}
∧ domain knowledge[c].visible = Colors
∧∀cc ∈ domain knowledge[c].visible : knowledge[c].visible[cc] ∈ Nat
∧ ∧ domain lower_bound = Colors
∧∀c ∈ domain lower_bound : lower_bound[c] ∈ Nat
That’s it! Plugging this into TLC will give us the result expected from the earlier proof: the model checker stops on the 101st day, with PopulationInvariant violated after all blue-eyed people leave on the 100th day.
6 Conclusion
Though presented sequentially, I actually went back and forth between the proof and the TLA+ model while working out how to formalize the solution to this logic puzzle. I found that switching between these tasks helped me think about the puzzle from different perspectives and kept me from getting stuck.
I found TLA+ especially useful as a way to double-check the logic of the proof and to look for off-by-one errors in how the number of days was calculated.
TLA+ is capable of a lot more, but I mostly find it useful as tool for building state machines. I really like its power in manipulating sets and how it models change as sequence of atomic, discrete steps. It may not be a tool to build something in the usual sense, but I find it especially valuable as tool to help me think and reason through new problems.