An ambiguous night knight

Chapter 6, Problem 6 from [To Mock a Mockingbird]

Here is a [calculational solution] to this problem.

In a vast underground world live two kinds of knights: day knights and night knights. Despite living underground, the knights know or feel whether it is day or night: the day knights always tell the truth by day and lie by night, and the night knights always tell the truth by night and lie by day.

Inspector Craig visits this world, and after several days he has lost track of day and knight. He meets a knight, who says: by day I say that I'm a night knight, but I am a day knight. Craig ponders this statement, and finds out what kind of knight it is, and whether it is day or night at that moment. Can you?

Representation

We write x for an arbitrary knight, and use the following notations:

 D.x == "x is a day knight"
 N.x == "x is a night knight"
 x/t<P.x.t> == "x says P.x.t on time t" (where t==true represents day,
                                         and t==false represents night)
 x/t{P.x.t} == "x can say P.x.t on time t"

The underground world can now be described by the following axioms: for every knight x and time-of-day t,

 (A) D.x =/= N.x
 (B) x/t<P.x.t> => x/t{P.x.t}
 (C) x/t{P.x.t} == D.x == t == P.x.t

First attempt at a solution

Let us call the knight that inspector Craig meets k, and let us call the time-of-day (represented as true for day and false for night) u. Then the situation can be described as follows:

 k/u< k/true{N.k} /\ D.k >

What can we derive from this? The calculation is straightforward:

   k/u< k/true{N.k} /\ D.k >
==   "simplify the inner expression first"

         k/true{N.k}
      ==   "axiom (C)"
         D.k == true == N.k
      ==   "axiom (A) and logic"
         false
         
   k/u< false /\ D.k >
==   "logic: simplify"
   k/u<false>
=>   "axiom (B)"
   k/u{false}
==   "axiom (C)"
   D.k == u == false
==   "logic: simplify"
   D.k =/= u

So we conclude that either k is a day knight and it is night, or k is a night knight and it is day. But we cannot be sure which of these is true! Therefore the problem is not correctly posed. Time for...

An alternative interpretation

Reading the answer that Mr Smullyan himself gives in his book, he interprets what the knight says as two statements: "by day I say that I am a night knight", and separately "I am a day knight". Formally:

 (1) k/u< k/true{N.k} >
 (2) k/u<D.k>

From this we can derive, again in a straightforward way:

   k/u<D.k>                                                  --- (2)
=>   "axiom (B)"
   k/u{D.k}
==   "axiom (C)"
   D.k == u == D.k
==   "logic"
   u

and:

   k/u< k/true{N.k} >                                        --- (1)
==   "simplify inner expression, see above"
   k/u<false>
=>   "the last three steps of the first attempt"
   D.k =/= u
==   "u == true, see above"
   !D.k

Hence it is day, and the knight is a night knight.

This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.

Changes to calc/tmam-6-6.html:

Mon Dec  6 08:47:17 MET 2004  Marnix Klooster
  * Corrected the 'alternative interpretation', which was completely wrong, giving exactly the wrong result.

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
  * Updated all files to use the m4 template

Sat Oct  6 15:43:25 MEST 2001  marnix
  * completed proof of ambiguous day knight problem

Fri Oct  5 21:08:28 MEST 2001  marnix
  * Added first part of the ambiguous day knight problem