A logic game in terms of Epistemic Logic with an implementation in Python

by N. Nikolopoulos

Consider the following game :

There are threeplayersand adeckwith 8 cards: 4 aces and 4 eights.

Each agent is dealt two cards and the remaining two cards are left face down. Assuming an ordering for the agents, they take turns trying to determine their own cards by looking at the cards of the others.

When a player is sure about his draw in his turn, he announces it, thus ending the game.

At first we need to define all available agents' draws :

**A**≔ agent_{i}*i*has a pair of aces**E**≔ agent_{i}*i*has a pair of eights**M**≔ agent_{i}*i*has a mixed draw

We also need to define the epistemic states aka worlds in the game :

A state is simply the draws for every agent, so it is simply a combination between agents' draws. But we should remember that there are eight cards in total, four for each kind, and that restricts the available choices. After some thought one should end up with the following set of epistemic states :

(AFinally, we may simplify the notation by taking into account the fixed agents' order, so that we call a world_{a},A_{b},E_{c}),(A_{a}, E_{b}, A_{c}), (A_{a}, E_{b}, M_{c}), (A_{a}, E_{b}, E_{c}), (A_{a}, M_{b}, E_{c}),(A_{a}, M_{b}, M_{c}), (E_{a},A_{b},A_{c}),(E_{a},A_{b},E_{c}), (E_{a},A_{b},M_{c}),(E_{a},E_{b},A_{c}), (E_{a},M_{b},A_{c}),(E_{a},M_{b},M_{c}), (M_{a},A_{b},E_{c}),(M_{a},A_{b},M_{c}), (M_{a},E_{b},A_{c}),(M_{a},E_{b},M_{c}), (M_{a},M_{b},A_{c}),(M_{a},M_{b},E_{c}), (M_{a},M_{b},M_{c})

`X`_{i}Y_{j}Z_{w}

as `XYZ`

.
`XYZ`

as nodes in an undirected graph. The graph has three types of edges :
- red edges that connect nodes which are the same (knowledge-wise) for agent
*a*i.e.`u`

_{1}∼_{a}u_{2} - green edges that connect nodes which are the same (knowledge-wise) for agent
*b*i.e.`u`

_{1}∼_{b}u_{2} - blue edges that connect nodes which are the same (knowledge-wise) for agent
*c*i.e.`u`

_{1}∼_{c}u_{2}

For instance, one can easily see above that states `AME,AMM`

are the "same" for agent
*c* since he shall see the same cards from the other two agents regardless of his own draw.

By the usual notation in modal logic, one could express the sentence e.g. "Agent *a* does not know his draw"
as `¬(K`

_{a}A_{a}∨K_{a}E_{a}∨K_{a}M_{a})

But what changes such an expression carries?

We could visualize this change by considering its negation i.e. if Agent *a* could know his draw.
If he could tell his draw, then the valid epistemic state could not be confused (by him) with another.
Consequently, the equivalence class for ∼_{a} would contain only one state. So we can safely
discard those states, since he cannot really tell his draw (we assume that the agents are not only logical, but
always truthful as well).

These changes are, of course, depicted in our graph by removing nodes (and their edges) accordingly. Also,
it is important to note that this new information modifies the agents' knowledge universally. For example,
in the first round agent *b*, after hearing that *a* cannot tell his draw, also knows that *a*
could not have seen two aces or two eights, so he can safely discard states `AEE,EAA`

as well.

Here is the structure after the first agent's announcement that he cannot tell his draw.

Using Python 3.8 we implemented the above graph
approach to the Aces & Eights Puzzle in this file. The whole puzzle is
represented by class `AcesEightsPuzzle`

where one can define different agents' names, the draw and
whether some output during the game is expected. We are using an undirected graph structure from module
*NetworkX*, its nodes are those described previously and the edges
of each agent shall be between nodes that share exactly two individual draws in their respective place (e.g.
for red edges we shall have `XME⟷YME,XMA⟷YMA`

etc).

Available functionality includes the removal of nodes for an Agent (after announcing his inability to
tell his draw, the simulation of the game for every round until an Agent is sure about his draw and the
visualization of the structure in any step of the game (with optional `.svg`

file production)
You can run the program by typing in your terminal `python aces_eights.py`

To test the program's validity we have developed a testing program that enables us to sanity check the methods' correctness. You can find that program here and test your own understanding on the puzzle by considering why each condition is valid. Why is an Agent able to tell (or not) in some state? Why these nodes shall be removed after this Agent announces that he cannot tell?