MAS: Using Priest Modal Tableaux to Visualise Kripke Models
Chapter 2: Theory
M. Koonstra S2399385 / G. Schoenmacker s1550748 / Rijksuniversiteit Groningen
Priest Semantic Tableaux
Semantic tableaux (sing. tableau) are a method for determining the validity of a formula by systematic representation of an argument and applying rules to this representation. More concretely, a semantic tableau is a tree of formulae combined with rules for expanding the tree using these formulae. The specific semantic tableaux method we used is taken from "An Introduction to Non-Classical Logic" by J. Priest. The images used below are taken from this book as well to demonstrate his methods (and thus, our methods).
Semantic Tableaux for Classical Logic
To prove whether a given formula is a tautology, semantic tableaux can be used. Consider the following formula:
((A → B) ∧ (B → C)) → (A → C)We can view this formula as an chain of reasoning with two premises and one conclusion. The method Priest employs add these premises to a tableau-tree and then adds the negation of the conclusion. If the formula is a tautology, this method should result in a closing of all possible semantic validations that could fulfil this tableau. The tree representation is depicted below. The bottom crosses are used to show that branch of the tree is closed, i.e. contains a contradiction.
Reasoning Rules for Classical Logic
The rules used to create the above tree are not evident from the example. The first thee formulae in the tree we can explain: these are the premises and the negation of the conclusion. After this, reasoning rules are used to expand the tree. Priest uses the following reasoning rules for classical logic:
 |
 |
 |
 |
|
 |
 |
 |
 |
 |
These rules are to be read as: When the formula above the arrow is encountered, add the formula(e) below the arrow to the tableau. If there are two arrows at the same level, a branch is created. An important observation here is that there is no one rule for negation: to expand a formula with a negation as its top operator, one need to look at the sub-formula to determine how the formula is to be expanded.
Semantic Tableaux for Modal Logic
The semantic tableaux representation presented above does not do for modal logic, in which we reason about multiple possible worlds. To extend the tableaux method to include modal semantics, Priest extends his modal tableaux to include a number for each formula representing the world in which the formula holds. The classical modal tableaux can be adapted to this new representation simply by adding a post fix '0' to each formula to indicate the formula is located in the same world. Relations between worlds are depicted as if they are formulae, using the irj notation to indicate i has a relation to j. The example below shows the following formula:
(
(A → B) ∧ (B → C)) → (A → C)
The expansion rules for classical logic are the same here as before. The now modal expansion rules are described in the following section.
Reasoning Rules for Modal Logic
Four new rules are introduced for modal reasoning:
The rules for negation are just rewriting rules and are relatively uninteresting. The rule for the box operator shows that two conditions must be met before the rule can be used: there must be some box formula in world i and there must be a relation irj. If these conditions apply, then we can introduce the relevant sub-formula in the world j. The rule for the diamond operator 
is interesting because it is the only rule that can introduce new worlds. This is the case because inherent in its semantics is the requirement that in some reachable world, its sub-formula holds true. Therefore there must be a reachable world. If a diamond-formula is encountered, a new world should be created which is connected from the current one and in this new world the sub-formula of the diamond formula must hold.
World relation rules in S5
S5 Kripke models are characterised by accessibility relations which are (1) reflexive, (2) symmetric and (3) transitive. Priest lists the following rules for these properties:
In short:
- Add relation iRi for any formula in world i (reflexivity)
- Add relation jRi for all relations iRj (symmetry)
- Add relation iRk for all relations iRj and jRk (transitivity)
These rules may introduce copies of already existing relations, so the additions are actually only carried out if the new relation does not exist yet.
Extending Priest for Multiple Agents
Something Priest does not cover in his book is the extension of logics to include multiple agents. The tableaux and expansion rules we have seen up to now, do not provide for logics with multiple agents. Using a presentation titled "Modified tableaux for some kinds of multi-modal logics" by Gomez-Caminero and Nepomuceno as inspiration, we modified our modal tableaux world relations to include information about agents. We adapted the modal reasoning rules as well to work with this new information.
The rules for modal logic do not change much due to this introduction. For clarity, we have included them below however. We introduce the new notation of 
and 
for saying "agent n knows" and "agent n thinks possible". The notation 
depicts a connection from world i to world j for agent n.
Extending with the E and C operators
To support the E and C operators, some new rules are introduced. Note that in the following image, the "n" stands for any agent. We introduce the new notation of 
and 
for saying respectively "every agent knows" and "it is common knowledge".
The E rule is not expanded by it's official definition but just applied as if it is a K rule for any agent. The negated E rule generates a branch for each agent in the system.
The official definition for common knowledge is as follows:
C A → E A ∧ EE A ∧ EEE A ...For this project, we have simplified this to the following to preventing recursive expansion of the rule:
C A → E(A ∧ C A)
Previous Chapter: Chapter 1 - Introduction
Next Chapter: Chapter 3 - Implementation
