We will treat this puzzle by assuming that there are
married couples in the country. Then
the language L = (Pr, Sp, T) adequate for this puzzle will be:
where denotes ith husband, means that
's wife is unfaithful and denotes
ith day.
Let denote that k-fold cartesian
product of the vector space with addition . We define
by ,
where and denotes
, resp.). We put and
.
We also use to denote arbitrary element in .
Now, let denote what the King publicized on the first day, and
denote a knowledge base
for under the situation .
Let us put:
and
where . We also put .
Then, as a formalization of the puzzle, we postulate the following
identities:
Since the meta-notions such as knowledge base and provability cannot be expressed directly in our language, we were forced to interpret the King's decree into in a somewhat indirect fashion.
Now, if we read Eq(*) as the definition of , then we find that the definition is circular, since in order that may be definable by Eq(*) it is necessary that are already defined, whereas are defined in terms of in . So, we will treat these equations as a system , , of equations with the unknowns and . We will solve under the following conditions:
(*) For any , is consistent.
(**) For any and , is a knowledge base for .
We think these conditions are natural in view of the intended meanings of and .
Let us define a norm on
by ,
where .
For any
and , we put
and for any , we put
We also put .
We define a KT5-model as follows:
Then we have the following theorem.
Theorem 8. Under the conditions () and (),
has the unique solution
,
where the solution is characterized by the condition:
Thus we have seen that may be regarded as the formal
counterpart of the King's decree in our
formal system. The puzzle is then reduced to the
problem of showing that:
We note that we can moreover prove the following:
It is clear that and follow at once from the condition stated
in theorem 8.