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:

contradiction?

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:

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:


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:


Modal logic tableau

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

method:


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


Example of tableau (3)

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 (2)


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:


Sequences of integers: rules

if F is the formula to check for satisfiability:


Sequences of integers: example (1)

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

as usual, tableaux work on sets of formulae


Sequences of integers: example (2)


Sequences of integers: example (3)

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) }

solution


Symbols for worlds

principles:


Symbols for worlds: rules

if F is the formula to check for satisfiability:


Symbols for worlds: example (1)

{ □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

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