MAS: Using Priest Modal Tableaux to Visualise Kripke Models

Chapter 4: Demonstration

M. Koonstra S2399385 / G. Schoenmacker s1550748 / Rijksuniversiteit Groningen

Demo

In this section we will show some of the possibilities of our program. This we will do by giving actual program output.

Tautologies

Currently our program can determine whether a formula is a tautology in classical logic and modal logic systems K and S5. Examples of this are:

The formula a | ~a is a tautology.
The formula p | (q & r) = (p | q) & (p | r) is a tautology.

The formula (K_1 a & M_1 b) > M_1 a is a tautology in K.
The formula (K_1 a & K_1 (a > b)) > K_1 b is a tautology in K.

The formula K_1 a > a is a tautology in S5.
The formula K_1 M_2 K_1 a > M_2 K_1 K_1 a is a tautology in S5.

One of these examples we shall look more closely at to show the inner workings of our program.

Examining Tree Branches

Here we shall investigate the actual branches our program produces when determining whether a formula is a tautology. For this we shall use the following example in system K:

(K_1 a & M_1 b) > M_1

To prove the above formula is a tautology in K (which it in fact is), our program produces the following branch:

~(K_1 a & M_1 b > M_1 a), w1
K_1 a & M_1 b, w1 (1)
K_1 a, w1 (2)
M_1 b, w1 (2)
~M_1 a, w1 (1)
K_1 ~a, w1 (5)
R_1w2, w1 (4)
b, w2 (4)
a, w2 (3, 7)
~a, w2 (5, 7)

The information and format presented is taken directly from our program, with the following alterations: (1) no line numbers are present in the program output; (2) the bold printed number between brackets at the end of a line shows the line number of the formula which generated this formula and has been added manually to aid readability; and (3) the order in which the formulae appear in the branch has been altered, again for readability.

When something is no Tautology

The really interesting process begins only when the prover has determined something to not be a tautology, because this means we can construct a counter model for visualisation. To show this, we will consider the following formula in K:

K_1 a | K_1 ~a

Obviously this is no tautology in K. When evaluating this model in system K(1), we see the following model:

This image is actual output of our program. It shows a model with three worlds: the world in which we evaluate our formula (labelled w1) and two connected worlds, one of which satisfies ~a and the other satisfying a. This is indeed a counter model of the example formula. This picture also shows our final goal: a visually clear representation of a counter model.

The same model we can also draw in S5(1). This is shown in the figure below. We can see the same formulae are valid in the same worlds, but also the reflexive, transitive and symmetric properties of S5.

Solving the Three Wise Men problem

To demonstrate the reasoning system and visualiser more in-depth, we will discuss the Three Wise Men problem which has been an assignment in the MAS-course. To reiterate: in this problem we have three perfect logicians (who also know each other to be perfect logicians) who get to wear a random hat drawn from a set of 3 red hats and 2 blue hats (known to everyone). They can each see the hats the other two are wearing, but not their own. Then they are repeatedly asked to step forward if they know the colour of their own hat.

Wise men background knowledge

The background knowledge for the model is as follows:

(b1 & b2) > r3
(b2 & b3) > r1
(b1 & b3) > r2

(b1 & ~r1) | (~b1 & r1)
(b2 & ~r2) | (~b2 & r2)
(b3 & ~r3) | (~b3 & r3)

In this example, b1, b2 and b3 respectively stand for the first, second or third wise man wearing a blue hat. Similarly, r1, r2 and r3 stand for the first, second or third man wearing a red hat. The first three lines formalise that no more than two blue hats can be worn: if we know two blue hats are worn, the third one must automatically be red. The second set of three rules formalise that each wise man must wear either a blue or a red hat. This is the background knowledge for this model.

In this example we have three situations:

All three men are wearing a red hat.
Two men are wearing a red hat, one wears a blue hat.
One man is wearing a red hat, two wear blue hats.

Wise men: the simple scenario

The third scenario is the simplest, so first we will ask our program what it can make of it. We create a S5EC model with three agents in which the background knowledge is common knowledge and one of the agents sees the other two wearing a blue hat. Then we ask whether is logically follows that the agent knows it is wearing a red hat:

C (
((b1 & b2) > r3) & ((b2 & b3) > r1) & ((b1 & b3) > r2) &
((b1 & ~r1) | (~b1 & r1)) & ((b2 & ~r2) | (~b2 & r2)) & ((b3 & ~r3) | (~b3 & r3))
)
#_1 (b2 & b3)
>
#_1 r1

The full formula we give out model is:

(C (((b1 & b2) > r3) & ((b2 & b3) > r1) & ((b1 & b3) > r2) & ((b1 & ~r1) | (~b1 & r1)) & ((b2 & ~r2) | (~b2 & r2)) & ((b3 & ~r3) | (~b3 & r3))) & #_1 (b2 & b3)) > #_1 r1

The program outputs the the formula is "a tautology in S5EC(3)". Also it shows 65 models for situations in which this formula holds. These models belong to one of three classes, one of each we will show here.

The largest group of models consists of models in which the program invalidates the background knowledge. Since the main formula is an implication, the program only has to find a situation in which the first sub formula of the implication does not hold to validate the implication. Therefore, the program constructs models in which the background knowledge is untrue. In the example above C((b1 & ~r1) | (~b1 & r1)) (which is part of our background knowledge) does not hold because agent 3 considers it possible that ~b1 & ~r1. We might consider this cheating, but this is a model in which the logical formula we gave the program holds.

Two counter models exist in which the program invalidates #_1 (b2 & b3), which is the second part of the conjunction (the first part being the common knowledge) in the first sub formula of the implication. If this is untrue, the implication by definition holds. Again, this is a valid but not very interesting model validating our formula.

Lastly, the program shows a single situation in which the first part of the implication holds. This is what we're interested in, because we assume the first part of the implication to be true in our story. Here we see the program need not create new worlds and can reason with the C and K operators in a single world, concluding what we know to be true: K_1 r1 holds and therefore r1 must be true.

In fact, the formula we chose is also a tautology in KEC(3). Should we however have concluded not that #_1 r1 but that r1, then the formula no longer holds in KEC(3). This is because of S5's reflexive property, in which knowledge implies truth.

Wise men: proving what cannot be known

In the above example, we assumed the third scenario (one man is wearing a red hat, two wear blue hats) to be true. Now, let's assume this is not the case, but instead all the men are wearing red hats. Now we can show that, if one man sees two red hats, that he cannot conclude what colour his hat is. First we will show that he cannot conclude he has a blue hat if he sees the other two wearing red hats:

(C (((b1 & b2) > r3) & ((b2 & b3) > r1) & ((b1 & b3) > r2) & ((b1 & ~r1) | (~b1 & r1)) & ((b2 & ~r2) | (~b2 & r2)) & ((b3 & ~r3) | (~b3 & r3))) & #_1 (r2 & r3)) > #_1 b1

The part which is different from the previous example is emphasised. If we process this formula, we will find that indeed the formula is no tautology in S5EC(3). A very large amount of counterexamples is produced. All of these basically boil down to the following:

In this counter model we can see agent 1 still considers it possible that he is not wearing a blue hat and therefore cannot know whether he is in fact wearing one.

Previous Chapter: Chapter 3 - Implementation

Next Chapter: Chapter 5 - Conclusions

Table of Contents - Top Of Page