AXIOMATIZATION OF MR. S AND MR. P

These axioms involve the same ideas as the wise man axiomatization. They are a debugged version of the axioms by Ma Xiwen of Peking University, which, in turn, were a variant of my earlier axiomatization.

This formalization separates the knowledge part of the problem from the arithmetic part in a neat way. Ma Xiwen verified, using FOL, that his axioms imply a certain purely arithmetic condition on the pair of numbers. It can be then shown that the only pair satisfying that condition is $4,13$.

$declare indvar t \in natnum;$

$declare indconst k0 \in pair;$

$declare indvar k\ k1 k2 k3 \in pair;$

$declare indconst RW \in world;$

$declare indvar w w1 w2 w3 \in world;$

$declare indconst S P SP \in person;$

$declare indvar r \in person;$

$declare opconst K(world)=pair;$

$declare opconst s(pair)=natnum;$

$declare opconst p(pair)=natnum;$

$declare predconst A(world,world,person,natnum);$

The predicates $Qs$, $Qp$, $Q1$, $Q2$, $R1$, $R2$ and $R3$ are represent arithmetic conditions on the pair of numbers that are used to express the arithmetic conditions on the pair that replace the knowledge conditions given in the problem statement.

$declare predconst Qs(pair) Qp(pair) Q1(pair) Q2(pair) Q3(pair);$

$declare predconst Bs(world) Bp(world) B1(world) B2(world);$

$declare predconst R1(pair) R2(pair) R3(pair);$

$declare predconst C1(world) C2(world);$

The first two axioms state that the accessibility relation is reflexive and transitive. They assert that what is known is true and one knows that one knows what one knows. Got that?

$axiom ar: \forall w r t.A(w,w,r,t);;$

$axiom at: \forall w1 w2 w3 r t.(A(w1,w2,r,t)\land A(w2,w3,r,t) \supset A(w1,w3,r,t));;$

This axiom says that the joint person knows what Mr. S and Mr. P both know. At first sight it seems too weak, but transitivity tells us that what they jointly know, they jointly know they jointly know.

$axiom sp: \forall w1 w2 t.(A(w1,w2,S,t)\lor A(w1,w2,P,t)\supset A(w1,w2,SP,t));;$

This next axiom is just a definition for the purposes of abbreviation. RW is the real world, so $k0$ is just the real pair.

$axiom rw: k0=K(RW);;$

In the initial situation they jointly know that Mr. S knows the sum and Mr. P the product. They also jointly know that this is all that Mr. S and Mr. P know about the numbers. This is asserted by saying that given any pair of numbers with the right sum, there is a world possible for Mr. S in which this is the pair of numbers.

$axiom init:$

$\;\forall w w1.(A(RW,w,SP,0)\land A(w,w1,S,0)\supset s(K(w))=s(K(w1)));$

$\;\forall w w1.(A(RW,w,SP,0)\land A(w,w1,P,0)\supset p(K(w))=p(K(w1)));$

$\;\forall w k.(A(RW,w,SP,0)\land s(K(w))=s(k)\supset \exists w1.(A(w,w1,S,0)\land k=K(w1)));$

$\;\forall w k.(A(RW,w,SP,0)\land p(K(w))=p(k)\supset \exists w1.(A(w,w1,P,0)\land k=K(w1)));;$

These axioms on the pair will be used to translate knowledge assertions. For example, $Qs(k)$ asserts that there is another pair that has the same sum as $k$ and is used in the assertion that Mr. S, knowing the sum, does not know the pair, i.e. does not know the numbers. As we proceed through the dialog the arithmetic conditions become more complex.

$axiom qs: \forall k.(Qs(k)\equiv \exists k1.(s(k)=s(k1)\land \lnot (k=k1)));;$

$axiom qp: \forall k.(Qp(k)\equiv \exists k1.(p(k)=p(k1)\land \lnot (k=k1)));;$

$axiom q:$

$\quad\quad\quad\quad \forall k.(Q1(k)\equiv \forall k1.(s(k)=s(k1)\supset Qp(k1)));$

$\quad\quad\quad\quad \forall k.(Q2(k)\equiv \forall k1.(R1(k1)\land p(k)=p(k1)\supset k=k1));$

$\quad\quad\quad\quad \forall k.(Q3(k)\equiv \forall k1.(R2(k1)\land s(k)=s(k1)\supset k=k1));;$

$axiom r:$

$\quad\quad\quad\quad \forall k.(R1(k)\equiv Qs(k)\land Q1(k));$

$\quad\quad\quad\quad \forall k.(R2(k)\equiv R1(k)\land Q2(k));$

$\quad\quad\quad\quad \forall k.(R3(k)\equiv R2(k)\land Q3(k));;$

$Bs(w)$ asserts that in the possible world $w$, Mr. S doesn't know the numbers.

$axiom bs: \forall w.(Bs(w)\equiv \exists w1.(A(w,w1,S,0)\land \lnot (K(w)=K(w1))));;$

$axiom bp: \forall w.(Bp(w)\equiv \exists w1.(A(w,w1,P,0)\land \lnot (K(w)=K(w1))));;$

$axiom b:$

$\quad\quad\quad\quad \forall w.(B1(w)\equiv \forall w1.(A(w,w1,S,0)\supset Bp(w1)));$

$\quad\quad\quad\quad \forall w.(B2(w)\equiv \forall w1.(A(w,w1,P,1)\supset K(w)=K(w1)));;$

$axiom c:$

$\quad\quad\quad\quad \forall w.(C1(w)\equiv Bs(w)\land B1(w));$

$\quad\quad\quad\quad \forall w.(C2(w)\equiv C1(w)\land B2(w));;$

The previous axioms were just definitions. Now we have the information coming from the dialog. SKNPK stands for ``S Knows that P does Not Know'' and the axiom asserts this about the real world at time $0$.

$axiom sknpk: B1(RW);;$

NSK stands for ``S doesn't know'', and the axiom asserts this about the real world.

$axiom nsk: Bs(RW);;$

PK stands for ``P knows the numbers'', and the axiom asserts this about the real world at time $1$.

$axiom pk: B2(RW);;$

SK tells us that at time $2$, Mr. S knows the numbers.

$axiom sk: \forall w.(A(RW,w,S,2)\supset K(RW)=K(w));;$

The last two axioms are the learning axioms. LS tells us that everyone learns by time $1$ that Mr. S knew at time $0$ that Mr. P didn't know the numbers, and he didn't know them either. LP tells us that everyone learns by time 2 that Mr. P knew the numbers by time $1$.

$axiom lp:$

$\;\forall w w1.(A(RW,w,SP,1)\supset (A(w,w1,P,1)\equiv A(w,w1,P,0)\land C1(w1)));;$

$axiom ls:$

$\forall w w1.(A(RW,w,SP,2)\supset (A(w,w1,S,2)\equiv A(w,w1,S,1)\land C2(w1)));;$

Ma Xiwen's proof was carried out using a sequence of lemmas. The first lemma shows the essential equivalence of a condition on possible worlds with a condition on pairs.

Lemma 1. $\forall w k.(A(RW,w,SP,0)\land k=K(w)\supset (Qs(k)\equiv Bs(w))).$

Lemma 2. $\forall w k.(A(RW,w,SP,0)\land k=K(w)\supset (Qp(k)\equiv Bp(w))).$

Lemma 3. $\forall w k.(A(RW.w.SP,0)\land k=K(w)\supset (Q1(k)\equiv B1(w))).$

Lemma 4. $\forall w k.(A(RW,w,SP,0)\land k=K(w)\supset (R1(k)\equiv C1(w))).$

Lemma 5. $R2(k0).$

Lemma 6. $\forall w k.(A(RW,w,SP,0)\land k=K(w)\supset (R2(k)\supset C2(w))).$

Lemma 7. $Q3(k0).$

Main Theorem. $R3(k0).$

$R3(k0)$ is a purely arithmetic condition on the pair of numbers. From an axiom asserting that $k0$ is a pair of numbers in the interval $2 \leq x \leq 99$ and Peano's axioms for arithmetic, the numbers can be proved to be $4$ and $13$. Alternatively, $R3(k0)$ can be translated into a computer program for computing the numbers. Most people who solve the problem write such a program.