Logic puzzle inspired by “Blue Eyes” I learned of the “Blue Eyes” puzzle for the first time a couple of weeks ago, and I’ve been playing around with some of the logical concepts behind it since then. For anyone unfamiliar with this puzzle, I suggest you read and solve it before trying this one.
My shenanigans led me to come up with the following puzzle (which I have, by now, already solved, but I have a feeling the MSE community will have fun with it):

An island has one blue-eyed person and one brown-eyed person, who can see each others’ eyes but not their own and cannot communicate. Every night, a ferry comes to take away any people who already know their own eye color. Both people are perfect logicians.
Prove that, for any $n\in\mathbb Z^+$, there exists a statement that you can announce to both of them so that they will both leave on night $n$ (no earlier and no later).

When I say “statement,” I mean this very generally. The method I used to prove this and construct such a statement for arbitrary $n$ was very messy and for large $n$ results in a “statement” that is very cumbersome to read (but logically coherent nonetheless).
 A: I'll put my solution in a spoiler, not to ruin it for anybody. It assumes that there are a countably infinite number of eye colours, though...
Announcement for $n=1$:

 For $n=1$, announce sentence $\varphi_1:=$ "there is one person with blue eyes, and one person with brown eyes." Both islanders will leave with the ferry the next night, for obvious reasons.

Announcement for $n=2$:

For $n=2$, announce: $\varphi_2:=$"if one of you has green eyes, the other has blue eyes, and if one of you has grey eyes, the other has brown eyes, and if neither of you have green or grey eyes, then $\varphi_1$."
Suppose I'm one of the islanders, and I can see blue eyes, then I know that I have either green or brown eyes. However, if I had green eyes, the other islander would leave the next night due to him knowing he has blue eyes. Therefore, since he didn't leave on the first night, I learn I must have brown eyes and will leave on night $2$. The same reasoning holds for the other islander.

Announcement for $n=3$:

For $n=3$, announce $\varphi_3:=$ "if one of you has purple eyes, the other has green eyes, and if one of you has red eyes, the other has grey eyes, and if neither of you have purple or red eyes, then $\varphi_2$."
Again, suppose I am the islander who sees blue eyes, then I know that neither of the colours can be purple or red (since then the other would be green or grey), thus $\varphi_2$ must hold.
From this, I know that I have either green eyes or brown eyes. In case I have green eyes, the other islander will think he has blue eyes or purple eyes, but does not know which, thus he can't leave on the first night. However, if the other islander had purple eyes, I would leave on the first night, which I don't. Hence on the second day, the other islander would know he did not have purple eyes and conclude he has blue eyes.
Therefore, if I had green eyes, the other islander would leave on the second night. Now, since the other islander didn't leave on the second night (for the same reason I didn't leave on the second night), I don't have green eyes, so I must have brown eyes, and hence I will leave on the third night.

Announcement for general $n\geq 2$:

We can keep doing this. Let $c_n$ and $c_n'$ be two colours that have not been used yet (so $c_1= blue$ and $c_1'=brown$, $c_2= green$ and $c_2'=grey$, $c_3=purple$ and $c_3'=red$). Then announce $\varphi_n:=$ "If one of you has $c_n$ eyes, the other has $c_{n-1}$ eyes, and if one of you has $c_n'$ eyes, the other has $c_{n-1}'$ eyes, and if neither of you have $c_n$ or $c_n'$ eyes, then $\varphi_{n-1}$."

