# Tableaux for modal logics

method for establishing the satisfiability of a formula

definition of satisfiability:

formula F is satisfiable if there exist M and s such that M,s ⊧ F

### Basic principle

a formula only is given

try to build a model M where F is satisfied in one of its worlds

### Facts

from examples we infer facts about modal logic

### First fact

is □x ∧ □¬x satisfiable?

proceed by intuition:

formula has to be true in a world s of a model M:

### First fact (2)

both □x and □¬x have to be true in that world:

### First fact (3)

in all successors of the state both x and ¬x are true:

looks unsatisfiable, but...

### First fact (4)

□x ∧ □¬x is satisfiable

just do not create any successor of s:

formula is satisfiable in a model comprising a single world
(regardless of the value of x in that world)

### First fact (5)

fact 1: do not create successors if not needed

rationale:

• after creating a successor, every formula like □F constrains F to be true in that successor
• more constraints = more chances of generating inconsistency
• save constraints by not creating successors

note: in some logics, creating a successor may be necessary
(e.g., logics with seriality)

### Second fact (1)

try to find a model for □x ∧ ◇¬x

### Second fact (2)

□x ∧ ◇¬x is satisfiable if there exists a model and a world s where it is true:

### Second fact (3)

 since □x ∧ ◇¬x is true in s, both □x and ◇¬x are true in s

### Second fact (4)

□x means: x true in all successors

by not creating successors, we avoid a constraint x on them

but ◇¬x is only true if the state has a successor where x is false

### Second fact (5)

 if ◇¬x is true in s s has a successor t where ¬x is true

### Second fact (6)

 since □x is true in s x is true in all successors of t in this case, x is true in t

formula is unsatisfiable

### Second fact (7)

fact 2: formulae ◇F impose the creation of successors where F is true
fact 3: once a successor is created, formulae □F act on it by creating a constraint F there

rationale:

• both facts are consequences of the semantics of modal logic
• fact 1 was only a guiding principle, facts 2 and 3 take precedence

### Fourth fact (1)

example: □x ∧ ◇y ∧ ◇¬y

### Fourth fact (2)

formula has to be true in a world s:

### Fourth fact (2)

 conjunction: all subformulae have to be true in the same world

### Fourth fact (3)

 for the moment, disregard boxed formulae concentrate on diamonds ◇y implies the existence of a successor t where y is true

### Fourth fact (4)

 ◇¬y requires a successor where ¬y is true try reusing the existing successor t

look inconsistent

but…

### Fourth fact (5)

 ◇¬y requires a successor where ¬y is true not necessarily the same one create a new successor instead

### Fourth fact (6)

left to do: □x makes x true in both t and q

no inconsistency

### Fourth fact (7)

fact 4: if possible, create different successors for different diamond formulae

notes:

• formulae are then imposed on different worlds,
decreasing chances of creating inconsistency
• in some modal logics, a world may be constrained to have a single successor
this fact do not apply then

### Modal logic tableau

we only consider modal logic K
(no constraint on the accessibility relation)

method:

• try to build the model satisfying the formula
starting from the world where the formula is true
• employ facts 1-4

### Example of tableau (1)

(x∧¬x)∨(□y∧◇¬y)

try to use the rules for propositional tableau as much as possible

### Example of tableau (2)

□y∧◇¬y has as the main connective

can still be expanded using the propositional rules

what now?

### Example of tableau (4)

rely on intuition for now

◇¬y means: ¬y true in a successor

formalization will be done later

### Example of tableau (5)

a successor of the initial state exists
□y implies that y is true there

### Example of tableau (6)

y cannot both true and false in the same state

close branch

### Formalization

requires:

1. expansion rules for and
2. a way of writing that something holds in a certain world
3. a way for specifying how these worlds are linked
(according to the accessibility relation)

points 2 and 3 explained on examples

### Specifying worlds

formula ◇x ∧ ◇¬x

tableau, informally:

by fact 4, the two successors are better be different

formalization has to include a way for specifying that formulae hold in different worlds

### Specifying the relation (1)

formula ◇¬x ∧ □◇x ∧ □□¬x

### Specifying the relation (3)

as usual: from ◇¬x to ¬x in a successor

### Specifying the relation (4)

the first boxed formula applies to the successor

### Specifying the relation (5)

◇x holds in the successor

a successor of it exists, and x holds in it

### Specifying the relation (6)

from box to the successor, again

### Specifying the relation (7)

box applies

contradiction: x and ¬x in the successor of the successor

### Specifying the relation (8)

the method has to keep track of where formula holds

also of the link between worlds

### Tableau for modal logics

three methods (in this course)

1. sequence of integers as labels
2. symbols as label
3. sets of formulae

differ on how they represent worlds and their relations

### Sequences of integers

rationale:

• worlds are represented by sequences of integers
example: (1,5,2) is a world
• the prefix tells successors and predecessor:
(1,5) is the predecessor of (1,5,2)
(1,5,2,3) is a successor of (1,5,2)
• formulae are labeled with sequences of integers
(1,5,4) x∧□y means that x∧□y holds in (1,5,4)

### Sequences of integers: rules

if F is the formula to check for satisfiability:

• propositional rules are as usual
world of consequence(s) same as that of precondition
• box:

 (i1,…,im) □F (i1,…,im,im+1) F

if (i1,…,im,im+1) is a sequence that is already in the tableau

• diamond:

 (i1,…,im) ◇F (i1,…,im,im+1) F

where im+1 is such that (i1,…,im,im+1) is a sequence that is not in the tableau yet

• closure: F and ¬F with the same sequence as label

### Sequences of integers: example (1)

{ □x ∧ ◇y, ◇(¬x ∨ ¬y) }

as usual, tableaux work on sets of formulae

expand

### Sequences of integers: example (4)

expand first

why (1,1)?

from (1) to (1,i) with i such that (1,i) is not already in the tableau

### Sequences of integers: example (5)

expand second

from (1) to (1,i)

but (1,1) already taken, use (1,2)

### Sequences of integers: example (6)

expand to (1,1)

note: can be done because (1,1) already exists

### Sequences of integers: example (7)

expand to (1,2)

note: can be done because (1,2) already exists

### Sequences of integers: example (8)

expand in (1,1)

note: from formula in (1,1) to formulae in (1,1)

### Sequences of integers: example (9)

(1,1) x and (1,1) ¬x contradict each other
(only because the world is the same: (1,1))

close branch

note: (1,2)y and (1,1)¬y not contradictory

### Sequences of integers: example (10)

no other expansion possible

set is satisfiable

model?

### Sequences of integers: example (11)

 consider the unclosed branch root ⟶ (sat) take only literals (no and, or, box or diamond) result: (1,1) x (1,1) ¬y (1,2) x (1,2) y

### Sequences of integers: example (12)

 (1,1) x (1,1) ¬y (1,2) x (1,2) y (seq) F means that F holds in world (seq) relation between worlds: (1,1) is a successor of (1) same for (1,2)

### Another example

{ □x, □(¬x∨□¬y), ◇(¬x∨◇y) }

### Symbols for worlds

principles:

• worlds are denoted by symbols w, w', w'', …
• formulae are labeled by the symbol of the world (as before)
• links between worlds is expressed by pseudoformulae wRw'

### Symbols for worlds: rules

if F is the formula to check for satisfiability:

• propositional rules as usual
world of consequence(s) same as that of precondition
• box:  w/□F   wRw' w'/F

preconditions are a labeled formula w/□F and a pseudoformula wRw'

• diamond:  w/◇F w'/F   wRw'

where w' is a new symbol
(a symbol not yet in the tableau)

generates a labeled formula w'/F and a pseudoformula wRw'

• closure: F and ¬F with the same label

{ □x, ◇¬x ∨ ◇x }

### Symbols for worlds: example (2)

begin with given formulae

### Symbols for worlds: example (3)

apply usual rule for disjunction

label of new formulae is the same

### Symbols for worlds: example (4)

a diamond formula generates a formula and a pseudoformula

### Symbols for worlds: example (5)

a box formula generates a new formula only in conjuction with an appropriate pseudoformula

### Symbols for worlds: example (6)

formulae are opposite to each other and the world is the same
close branch

### Symbols for worlds: example (7)

other branch: expand diamond

### Symbols for worlds: example (8)

other branch: expand box

### Symbols for worlds: example (9)

no further expansion possible

set is satisfiable

model?

### Symbols for worlds: example (10)

consider open branch
root ⟶ (sat)

take literals and pseudoformulae

w''/x, w''/x, wRw''

### Symbols for worlds: example (11)

w''/x, w''/x, wRw''

model:

### Set-based tableau

very different from previous ones

no labels

each node of the tree contains all formulae true in a world

propositional rules:
 A1…An,B ∧ C A1…An,B,C
 A1…An,B ∨ C A1…An,B | A1…An,C
modal rule:
 A1…An, □B1…□Bn, ◇C B1…Bn, C

principle: all box formulae and one diamond formula affect the successor

more than one diamond formula?

### More than one diamond formula

• branching
but not in the usual sense: branches are in "and", not "or"
• choose one

in the second case, a search in the space of tableau is needed
still in the "and" sense: satisfiable if no tableau can be closed

### Set based tableau: example (1)

{ z∨x, ¬z∧□x, □y, ◇z, ◇(¬x∨¬y) }

### Set based tableau: example (2)

first step: all formulae on the first node

### Set based tableau: example (3)

expand conjunction

break ¬z∧□x in two

### Set based tableau: example (4)

expand disjuction z∨x

two children: both contain all other formulae

### Set based tableau: example (5)

first leaf has z and ¬z: close

### Set based tableau: example (6)

expand diamonds

two children: each expand all boxes and one diamond

"and" branching: satisfiability is to be proved in both successors

### Set based tableau: example (7)

no expansion possible on first child

expand disjunction on second one

### Set based tableau: example (8)

both children contain a contraction

open branch: formula satisfiable?

### Set based tableau: example (9)

open leaf is on one way of an "and" branching

other way closes (all sub-branches close)

set unsatisfiable