I have completed a moderately formal proof of the proposition that, if there are
n blues and nobody leaves in the first
n-1 days, all blues will leave on the
nth day. It uses the day-indexed sequences of languages and theories discussed above.
Here's the proof and here's the
latex code.
My earlier proof was flawed, as pointed out by Maline. It turns out we do need to use more than one level of 'knows that...'. We don't need the unlimited number of levels that is implied by the concept of Common Knowledge though. We only need as many levels as there are blue nuns.
On day
n-1, the day they all leave, each blue has worked out she is blue because she knows what axioms the other nuns have on
previous days, and that on those days they deduced from those everything that is deducible, and she also knows that:
..on day n-2 nobody left and everybody knew that: (
... on day n-3 nobody left and everybody knew that: (
... on day n-4 nobody left and everybody knew that: (
...
... on day 1 nobody left and everybody knew that: (
... on day 0 nobody left and everybody knew that there was at least one blue) ... ) ) )
There are no circular references, because nuns only ever reason about what others knew
the previous day, not about what they know today. Each day's logical language is a meta-language of that of the day before, thereby avoiding circularity. We conduct our own reasoning, which includes a proof by mathematical induction, in a language that is meta to all the infinite sequence of languages, and hence can refer to them all.
I won't post the proof here, because it's eleven pages long and the latex would slow down the page rendering here too much. BUt here are the axioms I use:
The axioms of ##T0_0## are the axioms of Robinson Arithmetic and ZF set theory, plus the following scenario-specific axioms:
\begin{align}
&numBlue(0)\geq 1\\&
numLeave(d)=0\to (\forall m:\ \neg leaves(m,d))\\&
knowsSelfIsBlue(m,d)\wedge (\forall d'\leq d-1:\ \neg leaves(m,d'))\leftrightarrow leaves(m,d)\\&
knownMinBlue(d)\geq y+1 \wedge seesBlue(m,d)\leq y\to knowsSelfIsBlue(m,d)\\&
isBlue(0)\vee isBlue(1)\\&
isBlue(m)\wedge seesBlue(m,d)\geq y\to numBlue(d)\geq y+1\\&
numBlue(d+1)= numBlue(d)-numLeave(d)
\end{align}
(where ##(\forall x\leq a:\ F)## is shorthand for ##(\forall x:\ x\leq a\to F)## )
plus the following axiom schema that has one instance for each wff ##\theta## in ##L## with one free variable:
$$(\forall d'\leq d-1:\theta(d'))\wedge \theta(d)\to(\forall d'\leq d:\ \theta(d'))$$
where ##\theta(t)## denotes the formula generated by replacing the free variable by ##t## in ##\theta##.
For ##d\leq n-2##, the axioms of ##T0_{d+1}## are those of ##T0_{d}##, plus two extra axioms
\begin{align}
&d'\leq d\to numLeave(d')=0\\
&\phi(y)\to knownMinBlue(d)\geq y
\end{align}
Note that, since ##L_d\subset L_{d+1}## and ##T0_d\subset T0_{d+1}##, any wff of ##L_d## that is a theorem of ##T0_d## will also be a wff of ##L_{d+1}## and a theorem of ##T0_{d+1}##. We can write this in the meta-meta-language ##L^\ddagger## as:
$$(T0_d\vdash_{L_d} \theta)\to (T0_{d+1}\vdash_{L_{d+1}} \theta)$$
Finally, we also use a
private knowledge axiom in ##T1_d^m##, which states the number of blues that nun ##m## sees at 1pm on day ##d##.
Comments, suggestions, questions and criticisms are very welcome.
