Blue Eyes Can't Linger (A Logic Puzzle)

(Apologies for the not-witty Velvet Underground reference. Please suggest better titles in the comments.)

The Rapleaf blog recently posted a tough logic puzzle, which has apparently been around for a while. The XKCD writeup of the puzzle is a little clearer, IMHO. Both posts do a good job of describing the problem, so follow the links above for background.

The answer is: All 500 blue-eyed residents leave at midnight after the 500th day.

The solution was challenging enough to figure out, but even harder is the challenge of explaining why the solution is correct.

Fun. Here's my attempt:

(For these solutions, the day of the announcement is considered Day 1.)

Let's simplify things and start with 1 blue-eyed resident and 1 brown-eyed resident.

A visitor arrives and says: "I see someone with blue eyes."

Our blue-eyed resident looks around, doesn't see anyone with blue eyes, and realizes he must have blue eyes (I'm going to use the masculine pronoun just to keep things simple).

A: "I don't see anyone with blue eyes, so I must be the one with blue eyes."

B: "I see someone with blue eyes (A). No reason to think I have blue eyes."

Resident A leaves at midnight after Day 1.

2 blue-eyed and 2 brown-eyed residents.

A visitor arrives and says: "I see someone with blue eyes."

Day 1

A: "I see one person with blue eyes. That could be the person the visitor was talking about."

B: "I see one person with blue eyes. That could be the person the visitor was talking about."

C & D: "I see two people with blue eyes. Either could be the person the visitor was talking about."

Day 2

A: "B didn't leave, so he must see someone with blue eyes. That person must be me."

B: "A didn't leave, so he must see someone with blue eyes. That person must be me."

C & D: "A didn't leave because he saw B. B didn't leave because he saw A. No reason to think I have blue eyes."

A and B leave at midnight after Day 2.

3 blue-eyed and 3 brown-eyed residents.

A visitor arrives and says: "I see someone with blue eyes."

Day 1

A: "I see two people with blue eyes. Either could be the person the visitor was talking about."

B. "I see two people with blue eyes. Either could be the person the visitor was talking about."

C: "I see two people with blue eyes. Either could be the person the visitor was talking about."

D & E & F: "I see three people with blue eyes. Any one could be the person the visitor was talking about."

Day 2

A: "B didn't leave because he saw C. C didn't leave because he saw B. No reason to think I have blue eyes."

B: "A didn't leave because he saw C. C didn't leave because he saw A. No reason to think I have blue eyes."

C: "A didn't leave because he saw B. B didn't leave because he saw A. No reason to think I have blue eyes."

D & E & F: "A didn't leave because he saw B & C. B didn't leave because he saw A & C. C didn't leave because he saw A & B. No reason to think I have blue eyes."

Day 3:

A: "If there were only two residents with blue eyes, B and C would've left. They didn't so there must be a third. I see no other blue-eyed residents, so I'm the third."

B: "If there were only two residents with blue eyes, A and C would've left. They didn't so there must be a third. I see no other blue-eyed residents, so I'm the third."

C: "If there were only two residents with blue eyes, A and B would've left. They didn't so there must be a third. I see no other blue-eyed residents, so I'm the third."

D & E & F: "A, B and C should be figuring it out right now. No reason to think I have blue eyes unless they're here tomorrow."

A, B, and C leave at midnight after Day 3.

And so on, up to 500.