Notesale: Turn your study into money

Document Preview

Extracts from the notes are below, to see the PDF you'll receive please use the links above

---

MODAL LOGIC
For BS Students (Logical Paradigms in Computing)

This document contains detailed description of Modal Logic with solved exercises
...
It contains the topics
which are listed below:











Modal Logics and Agents
Semantics
Formulas and formula schemes
Equivalences between modal formulas
Logic Engineering
Correspondence Theory
Natural Deduction
Reasoning about knowledge in a multi-agent system
The modal logic KT45n
Natural deduction for KT45n

1|Page

Logical Paradigms in Computing
Modal Logics and Agents
Modes of Truth:
In propositional or predicate logic, formulas are either true, or false, in any model
...
In natural language, for example, we often
distinguish between various ‘modes’ of truth, such as necessarily true, known to be true, believed to be
true and true in the future
...
while true, and
maybe true for ever in the future
...
as well as being true is
also necessarily true and true in the future
...

In computer science, it is often useful to reason about modes of truth
...
For example, in artificial intelligence, scenarios with several interacting agents are
developed
...
So the task of the study is to look in depth at modal logics applied to
reasoning about knowledge
...
The
simplest modal logics just deal with one concept – such as knowledge, necessity, or time
...

Like negation (¬), they are unary connectives as they apply themselves to a single formula only
...
etc to denote atomic formulas
...


The following strings are not valid formulas:
Binding Property:
The unary connectives (¬, □ and ◊) bind most closely, followed by ∧ and ∨ and then followed by → and
↔
...
For example,□((◊q ∧¬r) → □p) can be written □(◊q ∧¬r → □p)
...

For example, in the logic that studies necessity and possibility, □ is read ‘necessarily’ and ◊ ‘possibly;’
in the logic of agent Q’s knowledge, □ is read ‘agent Q knows’ and ◊ is read ‘it is consistent with agent
Q’s knowledge that,’ or more informally, ‘for all Q knows
...
A set W, whose elements are called worlds;
2
...
A function L : W →P(Atoms), called the labelling function
...

These models are often called Kripke models
...
Suppose W equals {x1,x2,x3,x4,x5,x6} and
the relation R is given as follows:
R(x1,x2), R(x1,x3), R(x2,x2), R(x2,x3), R(x3,x2), R(x4,x5), R(x5,x4), R(x5,x6)
Suppose further that the labelling function behaves as follows:

Then, the Kripke model is illustrated in Figure given below:

Definition: Let M=(W, R, L)bea model of basic modal logic
...
The φ is true in the world x when x ⊩φ (satisfaction relation)
...
For ◊φ, it is
required that there is at least one accessible world in which φ is true
...

Definition: A model M=(W, R, L) of basic modal logic is said to satisfy a formula if every state in the
model satisfies it
...

Example: Consider the diagram given below:

3|Page

Formulas and formula schemes:
The family of formulas which have the same shape are called formula schemes
...

Any formula which has the shape of a certain formula scheme is called an instance of the scheme
...
In that
case, we say that Γ ⊨ ψ holds
...

We denote this by φ ≡ ψ
...
Indeed, if we take any
equivalence in propositional logic and substitute the atoms uniformly for any modal logic formula, the
result is also an equivalence in modal logic
...


The result of this substitution is the pair of formulas

which are equivalent as formulas of basic modal logic
...
e
...
A substitution instance of a formula is a valid formula
...


To proof of validity of first formula is given below: Suppose x is a world in a model M=(W, R, L)
...
e
...


Exercise
1
...
Draw a graph
for M
...
For the given pairs of formulas, can you find a model and a world in it which distinguishes them,
i
...
makes one of them true and one false? In that case, you are showing that they do not entail
each other
...
Justify your answer
...
The readings
related to □ are given below:
 Necessity
 Always in future
 Ought
 Belief
 Knowledge
 Execution of programs
We canalso engineer logics at the level of Kripke models
...
Let us start with necessity
...
The
meaning of R for each of the six readings of □ is shown in Table given below:

A given binary relation R may be:

Correspondence Theory
Definition: A frame F =(W, R) is a set W of worlds and a binary relation R on W
...
From any model we can extract
a frame, by just forgetting about the labelling function as shown below:
6|Page

Definition: A frame F =(W, R) satisfies a formula of basic modal logic φ if, for each labelling function
L : W →P(Atoms) and each w ∈ W the relation M,w ⊩ φ holds, where M=(W, R, L)
...

If a frame satisfies a formula, then it also satisfies every substitution instance of that formula
...

Properties of R corresponding to some formulas are in the table given below:

Theorem: A frame F =(W, R) satisfies a formula scheme in Table given above iff R has the
corresponding property in that table
...

The modal logic K:
The weakest modal logic doesn’t have any chosen formula schemes, like those given in above tables
...

The modal logic KT45:
A well-known modal logic is KT45 – also called S5 in the technical literature – where L = {T, 4, 5} with
T, 4 and 5 from Table given above
...
From tables given above:
T
...

4
...

5
...

Note that these properties represent idealisations of knowledge
...
Any sequence of modal operators and negations in
KT45 is equivalent to one of the following: −, □, ◊, ¬, ¬□ and ¬ ◊,where − indicates the absence of any
negation or modality
...
Correspondence theory
tells us that its models are precisely the Kripke modelsM=(W, R, L), where R is reflexive and transitive
...
For which of the readings of □ in Tables are the formulas below valid?
(φ → □φ) → (φ → ◊φ)

2
...
The main
difference is that we introduce a new kind of proof box, to be drawn with dashed lines
...
The dashed proof box has a completely different role from the solid
one
...
Going into a dashed box
means reasoning in an arbitrary accessible world
...
Then, we could work on this φ, to obtain, for example, ψ
...

 Wherever □φ occurs in a proof, φ may be put into a subsequent dashed box
...

□ Introduction

□ Elimination:

Note that there are no explicit rules for ◊, which must be written ¬□¬ in proofs
...
In the case of
KT45 some extra rules are required which are given below:

Since rule 4 allows us to move formulas beginning with □ into dashed boxes
...
Since 5 is a scheme and
since φ and ¬¬φ are equivalent in basic modal logic, we could write ¬φ instead of φ throughout without
changing the expressive power and meaning of that axiom
...
We
say that Γ ⱵL ψ is valid if ψ has a proof in the
natural deduction system for basic modal logic
extended with the axioms from L and premises
from Γ
...


9|Page

Exercise
1
...


2
...


10 | P a g e

Reasoning about knowledge in a multi-agent system
In a multi-agent system, different agents have different knowledge of the world
...
For example, in a bargaining situation, the seller of a car must consider what a buyer knows about the car’s
value
...

Reasoning about knowledge refers to the idea that agents in a group take into account not only the facts of the
world, but also the knowledge of other agents in the group
...


The modal logic KT45n:
We now generalise the modal logic KT45
...
,n} of agents
...
We assume a collection p,q,r,
...
The formula Ki p means that agent i knows p; so, for example, K1 p ∧ K1¬K2K1 p means that agent 1
knows p, but knows that agent 2 doesn’t know he knows it
...
The formula EG φ means everyone in the
group G knows φ
...
,n}, then EG p is equivalent to K1 φ ∧ K2 φ ∧ · · · ∧ Kn φ
...
Thus, EGEG φ is a state of knowledge even greater
than EG φ and EGEGEG φ is greater still
...
So we may
think of CG φ as an infinite conjunction

DG φ:
Finally, DG φ means the knowledge of φ is distributed among the group G; although no-one in G may know it,
they would be able to work it out if they put their heads together and combined the information
distributed among them
...
We simply write E, C and D without subscripts if we refer to EA,
CA and DA
...

We simplify by no longer requiring arrows on the links
...

Moreover, the relations are also reflexive, so there should be loops
...

Definition: Take a model M = (W, (Ri)i∈A, L) of KT45n and a world x ∈ W
...


Some valid formulas in KT45n:
The formula K holds for the connectives Ki, EG, CG and DG, i
...
we have the corresponding formula
schemes:

Observe that E, C and D are ‘box-like’ connectives, in the sense that they quantify universally over certain
accessibility relations
...
Write formulas for the following:
 Agent 1 knows p or agent 1 knows q
...

 Some people know p but don’t know q
...
Using the natural deduction rules for KT45n, prove the validity of the following sequents
...


13 | P a g e



---