next up previous
Next: References Up: The Puzzle of Unfaithful Previous: Informal presentation of the

Formal treatment of the puzzle

We will treat this puzzle by assuming that there are tex2html_wrap_inline692 married couples in the country. Then the language L = (Pr, Sp, T) adequate for this puzzle will be:
where tex2html_wrap_inline702 denotes ith husband, tex2html_wrap_inline700 means that tex2html_wrap_inline702's wife is unfaithful and tex2html_wrap_inline526 denotes ith day.

Let tex2html_wrap_inline708 denote that k-fold cartesian product of the vector space tex2html_wrap_inline711 with addition tex2html_wrap_inline714. We define
by tex2html_wrap_inline716, where tex2html_wrap_inline718 and tex2html_wrap_inline719 denotes tex2html_wrap_inline722, resp.). We put tex2html_wrap_inline724 and tex2html_wrap_inline725. We also use tex2html_wrap_inline728 to denote arbitrary element in tex2html_wrap_inline730. Now, let tex2html_wrap_inline458 denote what the King publicized on the first day, and tex2html_wrap_inline734 denote a knowledge base for tex2html_wrap_inline736 under the situation tex2html_wrap_inline738. Let us put:
where tex2html_wrap_inline410. We also put tex2html_wrap_inline746. Then, as a formalization of the puzzle, we postulate the following identities:



Since the meta-notions such as knowledge base and provability tex2html_wrap_inline748 cannot be expressed directly in our language, we were forced to interpret the King's decree into tex2html_wrap_inline458 in a somewhat indirect fashion.

Now, if we read Eq(*) as the definition of tex2html_wrap_inline458, then we find that the definition is circular, since in order that tex2html_wrap_inline458 may be definable by Eq(*) it is necessary that tex2html_wrap_inline760 are already defined, whereas tex2html_wrap_inline760 are defined in terms of tex2html_wrap_inline458 in tex2html_wrap_inline765. So, we will treat these equations as a system tex2html_wrap_inline767, tex2html_wrap_inline770, tex2html_wrap_inline772 of equations with the unknowns tex2html_wrap_inline774 and tex2html_wrap_inline458. We will solve tex2html_wrap_inline778 under the following conditions:

(*) For any tex2html_wrap_inline780, tex2html_wrap_inline782 is consistent.

(**) For any tex2html_wrap_inline780 and tex2html_wrap_inline736, tex2html_wrap_inline760 is a knowledge base for tex2html_wrap_inline736.

We think these conditions are natural in view of the intended meanings of tex2html_wrap_inline458 and tex2html_wrap_inline760.

Let us define a norm on tex2html_wrap_inline796 by tex2html_wrap_inline798, where tex2html_wrap_inline799. For any tex2html_wrap_inline802 and tex2html_wrap_inline804, we put
and for any tex2html_wrap_inline806, we put
We also put tex2html_wrap_inline808.

We define a KT5-model tex2html_wrap_inline810 as follows:


Then we have the following theorem.

Theorem 8. Under the conditions (tex2html_wrap_inline390) and (tex2html_wrap_inline836), tex2html_wrap_inline778 has the unique solution tex2html_wrap_inline840, where the solution is characterized by the condition:
Thus we have seen that tex2html_wrap_inline844 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 tex2html_wrap_inline846 and tex2html_wrap_inline848 follow at once from the condition stated in theorem 8.

next up previous
Next: References Up: The Puzzle of Unfaithful Previous: Informal presentation of the

Yasuko Kitajima
Fri Jun 20 13:39:43 PDT 1997