The island of blue eyed vampires (answer)
An initial idea
Each one needs to figure out if him/herself is blue eyed. They assume having blue eyes and see how the others react.
A technical details
There are some variations to formalize this problem using different type of logic: modal logic, temporal logic, Public Announcement Logic and so on.
I believe that those kind of prove are tedious to write and read. For now, I will write a sketch to a prove but I belive the best way to prove is using an algorimthm what basically, it would be an adaptation of DPLL algorithm (Davis–Putnam–Logemann–Loveland) that uses dedutive reasoning and prove by contraction.
Legend
\[\begin{matrix}
BlueEyed(X) :X \text{ is blue eyed.} \\
Leave(X) :X \text{ leaves.} \\
O(y) :y \text{ holds at the next (temporal) state.}
\end{matrix}\]
In this temporal simplified logic, we have a set of state that holds the in- formation of days, \(W = \{d_0, d_1, d_2, d3 \ldots , d_n\}\) and transition \(S : W \rightarrow W = \{(d_0, d_1),(d_1, d_2),(d_2, d_3), \ldots(d_{n−1}, d_n)\}\) (it means, one day is followed by the next). For any subject \(X\), \(X\) want to know if himself can leave. As soon \(X\) realize that he/she can leave he/she will leave.
Now, we want to create a “frame” with the knowledge of a specific subject in a certain point of time. But in our process, one subject will reason about what another is thinking in a recursive way (in the similar process as the minimax algorithm).
As the day follows,
\[\begin{matrix}
d_i & | & O(\phi) \\
d_{i+1} & | & \phi
\end{matrix}\]
In a frame of day \(d_i\) of subject \(X\):
\[BlueEyed(X) \Rightarrow O(Leave(X))\]
But, as the problem was announced no subject leave until \(n^{\text{th}}\) - last day: \[\begin{matrix}
\forall X, i < n, d_i \square_X & | & \neg Leave(X)
\end{matrix}\]
Two vampires example
Let us assume only two vampires: Anna and Maria. Both vampires know
\[\begin{matrix}
BlueEyed(Maria) \vee BlueEyed(Anna)
\end{matrix}\]
Now, let us examine Maria reasoning, \(\square_{\text{Maria}}\)... \[\begin{matrix}
\neg BlueEyed(Maria) & \text{(hypothesis)} \\
BlueEyed(Anna) & \text{(unit propagation)} \\
O(Leave(Anna)) & \text{(prognosis: next day Anna leaves)}
\end{matrix}\]
However, next day, Anna did not leave (what is a contradiction \(\bot\) - hypothesis is false). Therefore,
\[\begin{matrix}
\vDash BlueEyed(Maria) & \text{(law of the excluded middle)}
\end{matrix}\]
Three vampires example
Now let’s do that for 3 vampires: Anna, Maria and John.
Global knowledge
\[\begin{matrix}
BlueEyed(Maria) \vee BlueEyed(Anna) \vee BlueEyed(John) \\
BlueEyed(X) \Rightarrow O(Leave(X))
\end{matrix}\]
At, any time, there are 3 frames…: (frame 1) What Maria is thinking…(frame 2) What Maria thinks what Anna is thinking and (frame 3) What Maria thinks what Anna thinks what John is thiking.
Maria hypothesis is \(\neg BlueEyed(Maria)\). But she also KNOWS (\(\Rightarrow\) she is SURE about that) that Anna would be thinking the same way. So, if Maria hypothesis is right, for Anna, Maria would be not BlueEyed. At same time, Anna would be considering herself as not blue eyed by her own hypothesis. And, applying the same reasoning, Anna would consider what John would be thinking. And that third frame would inheritated not blue eyed for Maria and not blue eyed for Anna. Therefore, John would know that he is the only one with blue eyes and for Anna (according with Maria reasoning) the conclusion would be that John leaves next day.
However, John would not leave. So, Anna hypothesis was wrong (in frame 2). So, in frame 2, Anna concludes that she has blue eyes. But next day Anna does not leave. So Maria concludes that she must have blue eyes.
\[\begin{matrix}
& BlueEyed(Maria) ∨ BlueEyed(Anna) ∨ BlueEyed(John) \\
& BlueEyed(X) \Rightarrow O(Leave(X)) \\
d_0| & \neg BlueEyed(Maria) & \text{(Maria hypothesis)} \\
d_0| & \neg BlueEyed(Anna) & \text{(Anna hypothesis over Maria hypothesis)} \\
d_0| & BlueEyed(John) & \text{(unit propagation)} \\
d_0| & O(Leave(John)) & \text{(prognosis)}
\end{matrix}\]
The next day prognosis…\[\begin{matrix}
d_1| & Leave(John) &
\end{matrix}\]
at \(d_1\) …
\[\begin{matrix}
d_1| & \neg Leave(John) \bot \\
d_1| & BlueEyed(Anna) & \text{(law of the excluded middle)} \\
d_1| & O(Leave(Anna)) & \text{(prognosis)}
\end{matrix}\]
So \[\begin{matrix}
d_2 & Leave(Anna) & \text{(prognosis)}
\end{matrix}\]
at \(d_2\) …
\[\begin{matrix}
d_2|& \neg Leave(Anna) \bot \\
d_2 & \vDash BlueEyed(Maria)
\end{matrix}\]
Comentários