Modal logics

propositional logic

statements that can be true or false

modal logic

statements on sets of different scenarios

Propositional vs. modal: example

Propositional vs. modal: difference

propositional

statements refer to a single, specific case

modal

several different possibilities are considered
statements may refer to one, but also to a number of them

Modal logics: syntax

recursively defined from:

• variables
• ¬, ∧, ∨
• ◇, □

the modal operators □ and ◇ are applied to a single formula,
which may contain ¬, ∧ and ∨ but also other ◇ and □

examples:

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

usual recursive definition of syntax
(variable is a formula, if A and B are two formulae then A ∧ B is a formula, etc.)

Precedence

unary operators ¬, □ and ◇ have the same precedence

they take precedence over the binary connectives ∧ and ∨

therefore, □x ∨ y is:

• the same as (□x) ∨ y
• different from □(x ∨ y)

Diamond

◇ is complementary to □

□x

means that x is true in all considered situations

◇x

means that x is true in at least one of the considered situations

depending on the application, ◇x therefore may mean:

• that x is true at least one of the scenarios considered possible
• that x will be true at some future time
• …

it holds ◇F=¬□¬F

Semantics

□F means that formula F is true in various situations

cannot be evaluated with a single interpretation
(an interpretation represents one situation)

evaluating a formula requires not just an interpretation, but a set of interpretations

semantics is complicated
varies with the application

Two modal logics

(others exist)

• truth in a set of possible scenarios (S5)
• truth in the future (TL: temporal logic)

evaluating a formula requires:

S5

truth in a set of scenarios
□F means that F is true in all scenarios considered possible
required to evaluate a formula: a set of propositional interpretations
(describing the possible scenarios)

TL

truth in the future
□F means that F is true now and forever
required to evaluate a formula: a sequence of interpretations
(describing the state at each time point)

Semantics: generalization

in both cases:

in order to evaluate a modal formula, a set of interpretations is required

they differ because:

interpretations are given as a set (S5), or as a sequence (TL)

Kripke model: a generalization including both, but also many other ones

Kripke model

• a set of possible worlds
• a propositional interpretation for each world
• information on how the worlds are linked,
  depends on the application, like:
  • S5: all linked to all
  • TL: linked to form a line (more or less, details later)

What is a "world", exactly?

the set of possible worlds is a set of elements

is not a set of propositional interpretations

why not?

Couldn't this be simplified?

worlds are just elements of a set…

… but then a propositional interpretation is associated to each world

why not defining a model to be: a set of interpretation plus their links?

Different worlds, same interpretation

for S5, the simplified definition would work:
no point in having two worlds with the same interpretation

in TL, it does not:
two different time points may have the same interpretation
(example on the next slide)

Different worlds, same interpretation in TL

two different time points may have the same interpretation

example: the sequence of states:

ab, ¬ab, a¬b, ab, ab, ab, …     (ab forever)

interpretation ab recurs in different time points (worlds)

□a is false in the first state, but true in the fourth

state one and state four have the same interpretation,
but
a modal formula evaluates differently on them

Kripke model, formal definition

⟨R,S,V⟩

• S is a set (the set of possible worlds)
• V is a function from S to the set of propositional interpretations
  (the values of the variables in that world)
• R is a relation on S
  = a subset of S×S (the links between worlds)

what is the relation?

how is it used?

Accessibility relation

intuition: □F means that F is true in a set of worlds

• S5: all worlds
• TL: the future worlds

both cases can be encoded using the right accessibility relation

• S5: the relation links all worlds
• TL: the relation links each world with all ones in its future

the point: the relation tells the worlds to look when evaluating □F (cont.)

Evaluation

formulae are evaluated in a model and one of its worlds

x is true in ⟨R,S,V⟩,s

if x is true in the propositional interpretation V(s)

F∧G is true in ⟨R,S,V⟩,s

if both F and G are true in ⟨R,S,V⟩,s
(same for ∨ and ¬)

□F true in ⟨R,S,V⟩,s

if F is true in ⟨R,S,V⟩,s'
for all s' ∈ S such that ⟨s,s'⟩ ∈ R

notation: ⟨R,S,V⟩,s ⊧ F

(diamond: later)

Evaluation, in words

formulae are evaluated recursively in the same state except for boxed formulae

for boxed formulae, evaluate subformula in all linked states

in all worlds linked from s formula F is true ⇒ □F is true in s

Evaluation, example

truth in s:

• ¬a true in s
  (because the interpretation of s evaluates a to false)
• ¬a ∨ b true in s
  (because ¬a is true in s)
• □b true in s
  (because s is linked to s' and s''', and b is true in both)
  (note that □b is true in s, where b is false)
• □a false in s
  (because s is linked to s''', where a is false)
• □¬a false in s
  (because s is linked to s', where ¬a is false)
  (note that both □a and □¬a are false in the same state s)

Evaluation, example

truth in s':

• □¬a false in s'
  (because s' is linked to s' itself, where ¬a is false)
  (note that loops are to be taken into account)
• □b true in s'
  (because s' is linked to s' and s'', and b is true in both)

Truth in a model

a formula is true in a model if it is true in all states of the model

formally: ⟨R,S,V⟩ ⊧ F if ⟨R,S,V⟩,s ⊧ F for all worlds s∈S

Diamond

◇F is true in s if F is true in a world s' such that ⟨s,s'⟩∈R

F is true in one world reachable from s   ⇒   ◇F is true in s

one world is enough!

Models and applications

not all models are right for all kinds of applications:

S5

only models where R=S×S
each model linked to each other

TL

R forms a "row" of states (+transitivity)

Assumptions on models and truth

the same formula may be true in all models of a logic but not of another

example: ◇F → □◇F

• always true in S5
• may be false in TL (depends on the model)

Formula in S5

◇F → □◇F always true: proof

(for simplicity, we use lines in place of arrows;
can be done because the relation is symmetric)

(loops omitted)

◇F is true in a world s ⇓ there exists s' where F is true

Formula in S5 (2)

for every other s'', it holds ⟨s'',s'⟩∈R ⇓ ◇F is true in all worlds

Formula in S5 (3)

◇F is true in all words; as a result, □◇F is true as well (whichever world we choose, ◇F is true in all linked ones)

Formula in TL

◇F → □◇F false in TL: proof

counterexample:

loops and arcs that follow from transitivity omitted
(shown only when necessary)

Formula in TL (2)

F is true in the third state
reachable from initial state
⇓
◇F true in the initial state

Formula in TL (3)

F false from fourth state on
⇓
◇F false in the fourth state

Formula in TL (4)

◇F false in the fourth state
reachable from the initial state
⇓
□◇F false in the initial state

conclusion: ◇F → □◇F false

Formulae and logics

◇F → □◇F is:

• always true in S5
• false on at least a model of TL

validity depends on the assumptions on the relation R
(which vary with the logic: S5 or TL, in the example)

Conditions on relations

for simplicity, ⟨s,t⟩ ∈ R is denoted as sRt

the accessibility relation may be:

• reflexive: sRs for every s
• symmetric: if sRt then tRs
• serial: for every s there exists t such that sRt
• transitive: if sRt and tRu then sRu
• …

some formulae are true in all models only if some assumptions hold

Reflexivity and truth

some formulae are always true only if the relation is reflexive

• □F → F is true if the relation is reflexive:

  since □F is true in the state, F is true in all its successors

  but the state is one of the successors of itself, therefore F is true there

• in general, it is not:

  in the left state, □F is true
  because F is true in the only successor

Symmetry

• F → □◇F is true on symmetric relations:

  since F is true, in every predecessor ◇F is true but the predecessors are also the successors therefore, in all successors of the state ◇F holds

Seriality

• □F → ◇F is true on serial relations:

  if □F is true in s,
  and every state has a successor t,
  then F is true in t;
  therefore, F is true in at least a successor of s

  does not hold on states having no successors:

  s has no successors ⇒ F is true on all its successors but it has no successors ⇒ F is not true in one of them

Truth and assumptions on R

conclusion:

some formulae are always true only if the relation satisfies certain conditions

Truth in a modal logic

every modal logic (S5, TL, …) is specified by the assumptions on the accessibility relation

a formula is true in a logic if it is true in all models whose relation satisfies the corresponding assumptions (e.g., reflexivity, transitivity, …) of that logic

K is the modal logic with no assumption on the relation

Satisfiability

formula F is satisfiable if there exist ⟨R,S,V⟩ and s such that ⟨R,S,V⟩,s ⊧ F

where:

• s ∈ S
• R satisfies the conditions dictated by the particular modal logic under consideration

by the second point, satisfiability depends on the considered modal logic