Epistemic logics: an introduction

V Goranko

Epistemic logics: an introduction

Valentin Goranko Technical University of Denmark

DTU Informatics

November 2010

V Goranko

Modal reasoning about knowledge and belief

• Epistemic reading of the modal operators:

2ϕ: ‘the agent knows thatϕ’;

3ϕ: ‘ϕis consistent with the agent’s knowledge’.

• Doxastic reading of the modal operators:

2ϕ: ‘the agent believes thatϕ’;

3ϕ: ‘ϕis consistent with the agent’s beliefs’.

• Knowledge is always true, while beliefs need not be.

V Goranko

Epistemic logic: syntax and basic principles

Language of EL: just like the basic modal logic, but with the knowledge operatorKinstead of2. Formulae:

ϕ=p | ⊥ | ¬ϕ|ϕ∧ϕ|Kϕ

The other propositional connectives: definable as usual.

No special notation for the dual ofK.

Some basic principles of EL:

K K(φ→ψ)→(Kφ→Kψ)

T Kϕ→ϕ (knowledge is truthful) 4 Kϕ→KKϕ (positive introspection) 5 ¬Kϕ→K¬Kϕ (negative introspection) Thus, EL is in fact the modal logic of equivalence relations S5.

Problem: logical omniscience.

V Goranko

Kripke models for the epistemic logic

• Epistemic frame: a pair (W,R), where:

• W is a non-empty set of possible worlds, representing the possible states of affairs in the actual world.

• R⊆W² is an equivalence relation, calledepistemic indistinguishability relationbetween possible worlds.

• epistemic model: M= (W,R,V) where (W,R) is an

epistemic frame andV :AP→ P(W) is avaluation assigning to every atomic proposition the set of possible worlds where it is true.

The idea of the epistemic indistinguishability relation:

s1Rs2

holds if, from all that the agent knows, he cannot distinguish the statess₁ and s₂. In other words, at the state s₁ the agent considerss2 equally possible to be the case.

V Goranko

Kripke semantics of the epistemic logic

The semantics for EL is the usual Kripke semantics. In particular:

M,s |=Kϕ iffM,t |=ϕfor every statet such thatsRt

Meaning: the agent knowsϕat the possible world s ifϕ is true at every possible worldt that is indistinguishable froms by the agent.

That is, the agent knowsϕat the possible world s if (s)he has no uncertainty about the truth ofϕ at that world.

V Goranko

Epistemic models: example 1

Consider a language with two atomic propositions,p andq. Consider the modelM(the reflexive loops are omitted):

s1

{p,q}

s2

{p}

s3

{q}

s4

{}

s5

{p}

• M,s1 |=p∧Kp; M,s1 |=q∧ ¬Kq; M,s1 |=KKp∧K¬Kq.

• M,s₃ |=q∧ ¬p∧ ¬Kq∧ ¬K¬p∧K(¬Kq∧ ¬K¬p).

V Goranko

Epistemic models: example 2

See Pacuit’s slides.

V Goranko

Multi-agent epistemic reasoning: a prelude

Suppose now that there are two agents, Ann and Bob.

We associate knowledge operators with each of them.

• K_Ap: “Ann knows that p”.

• K_Bp: “Bob knows that p”.

• K_AK_Bp: “Ann knows that Bob knows that p”.

• K_ABp:=K_Ap∧K_Bp: “Both Ann and Bob know that p”.

• There can be many agents.

So, let Ep mean “Everybody knows thatp”.

• Then EEp: “Everybody knows that everybody knows that p”.

• EEE. . .p mean “Everybody knows that everybody knows that that everybody knows . . . that p”.

That means “p is a common knowledge”.

V Goranko

Multi-agent epistemic operators

Framework: a set of agents (players)Ag, each possessing certain knowledge about the system, the environment, themselves, and the other agents.

Multi-agent epistemic logics: multi-modal logics withepistemic modalitiesfor agents and groups (coalitions) of agents.

• K_iϕ: ‘The agenti knows thatϕ’.

• K_Aϕ: ‘Every agent in the groupA knows thatϕ’.

• D_Aϕ: ‘It is adistributed knowledge amongst the agents in the group Aimplies that ϕ’.

or, ‘The collective knowledge of all agents in the groupA implies that ϕ’.

• CAϕ: ‘It is a common knowledgeamongst the agents in the group Athat ϕ’.

V Goranko

Multi-agent epistemic operators: distributed knowledge

The idea: if Agent 1 knowsϕ and Agent 2 knowsψ, then they together can deriveϕ∧ψ, i.e. D1,2ϕ∧ψ holds.

Important concept indistributed computing.

V Goranko

Multi-agent epistemic operators: common knowledge

Intuitively,ϕis a common knowledge amongst the agents inAif K_Aϕholds, andK_AK_Aϕholds, and K_AK_AK_Aϕholds, etc. – infinitely!

This cannot be reduced to a finite chain.

Example: the coordinated attack problem.

V Goranko

The coordinated attack problem

• Two allied armies are on the two sides of a mountain, and their common enemy is in a fortress on top of the mountain.

• Neither army can defeat the enemy alone, and both army commanders know that. So, they have to attack together.

• There are two options for the simultaneous attack: at down or at night.

• The two commanders must coordinate the time of the attack, by confirming their choice between themselves.

• That is,the time of the attack must become their common knowledge!

• Their only means for communication is by sending messengers to each other.

• Can the attack be coordinated reliably?

V Goranko

The muddy children problem

See Pacuit’s slides.

V Goranko

Multi-agent epistemic logic (MAEL): formal syntax

Formal syntax:

ϕ:=p| ¬ϕ|ϕ∨ψ|K_iϕ|K_Aϕ|C_Aϕ|D_Aϕ, wherei is an agent,Ais an arbitrary set of agents, and Ki,KA,CA,DA are epistemic modal operators respectively for individual, group, common, and distributed knowledge of agents and coalitions.

V Goranko

Multi-agent epistemic logic:

expressing some epistemic properties

ICompare: ¬K₁ϕ and K₁¬ϕ

I“Agent 1 does not know whetherϕis true:” ¬K₁ϕ∧ ¬K₁¬ϕ I“The knowledge of agent 1 aboutϕis consistent:”

K₁ϕ→ ¬K₁¬ϕ

I“Agent 2 knows that agent 1 does not know whetherϕis true:”

K₂(¬K₁ϕ∧ ¬K₁¬ϕ) I K_{1,2}ϕ∧K_{1,2}K_{1,2}ϕ∧ ¬C_{1,2}ϕ

“Both agents 1 and 2 know thatϕis true, and they both know that they both know it, but the truth ofϕis not a common knowledge between them”.

I ¬K₁ϕ∧ ¬K₂ϕ∧C{1,2}(¬K₁ϕ∧ ¬K₂ϕ)∧D{1,2}ϕ

“None of the agents 1 and 2 knows thatϕis true, and that is a common knowledge between them, but the truth ofϕis

distributed knowledge between them”.

V Goranko

Using Multi-agent epistemic logic: the 3 cards scenario

There are 3 cards: A(ce),K(ing) and Q(ueen) and three persons:

1,2,3. Each of them holds one of the cards and does not know the cards of the other two.

To describe the situation in MAEL, we introduce propositions:

P_i,A,P_i,K,P_i,Q, for i = 1,2,3, whereP_i,A means that the personi holds the cardA, etc. Here are some true formulae:

IP_1,A∨P_2,A∨P_3,A; P_1,A∨P_1,K ∨P_1,Q;

IK_{1,2,3}(P_1,A∨P_2,A∨P_3,A); K_{1,2,3}(P_1,A∨P_1,K ∨P_1,Q);

IC_{1,2,3}(P_1,A∨P_2,A∨P_3,A); C_{1,2,3}(P_1,A∨P_1,K ∨P_1,Q);

IPi,A →KiPi,A; C{1,2,3}(Pi,A →KiPi,A); ¬P_i,A →Ki¬P_i,A; IP_1,A →K₁¬P_2,A∧ ¬K₁P_2,K ∧ ¬K₁P_2,Q;

ID_{1,2}P_3,A∨D_{1,2}P_3,K ∨D_{1,2}P_3,Q; IC_{1,2,3}(P_1,A∧P_2,K →D_{1,2}P_3,Q).

V Goranko

Multi-agent epistemic logic: Kripke models

Multi-agent epistemic model:

M=hS,Π, π,Ag,∼₁, ...,∼_ni, where:

• S is a set ofstates,

• Π is a set of atomicpropositions,

• π :S→2^Π is a valuation,

• Ag={1, ...,n}is a finite set of agents,

• ∼₁, ...,∼_n – the epistemic indistinguishability relations associated with the agents.

V Goranko

Multi-agent epistemic logic: formal semantics

The formal semantics of the epistemic operators at a state in a multi-agent epistemic model

M=hS,Π, π,Ag,∼₁, ...,∼_ni is given by the clauses:

(K_i) M,q |=K_iϕ iff M,q⁰|=ϕ for allq⁰ such that q∼_iq⁰.

(K_A) M,q |=K_Aϕiff M,q⁰ |=ϕfor all q⁰ such thatq ∼^E_A q⁰, where∼^E_A=S

i∈A ∼_i.

(C_A) M,q |=C_Aϕiff M,q⁰ |=ϕfor all q⁰ such thatq ∼^C_A q⁰, where∼^C_A is the transitive closure of ∼^E_A.

(D_A) M,q |=D_Aϕiff M,q⁰ |=ϕfor all q⁰ such that q ∼^D_A q⁰, where∼^D_A=T

i∈A ∼_i.

V Goranko

Epistemic model updates

• Epistemic models represent the static knowledge of the agents at a given moment.

• When the knowledge of any agent changes, the model must be updated to reflect that change.

• These updates are studied by Dynamic epistemic logic.

• For instance, the knowledge of agents changes as a result of communication.

• A simplest form of communication ispublic announcement.

It creates a common knowledge amongst all agents of the truth of the publicly announced fact.

• The model update after public announcement of the truth of ϕis simple: remove all states whereϕis false.

V Goranko

Modeling and solving the muddy children problem

See Pacuit’s slides.

V Goranko

Axioms for the basic multi-agent epistemic logic S5

The multi-modal logicS5_n is a multi-modal version ofS5.

The axioms ofS5n:

K Ki(φ→ψ)→(Kiφ→Kiψ) T K_iϕ→ϕ (knowledge is truthful) 4 K_iϕ→K_iK_iϕ (positive introspection) 5 ¬K_iϕ→K_i¬K_iϕ (negative introspection)

Inference rules: for each i:

ϕ K_iϕ.

V Goranko

Axioms for common and distributed knowledge

MAELnextends S5n with the following schemes for each A⊆Ag:

IThe axioms forK_A: K_Aϕ↔V

i∈AKiϕ;

I(Least) fixed point axioms forC_A:

LFP_A : C_Aϕ↔(ϕ∧K_AC_Aϕ), I Axioms forDA:

S5(DA) : The S5 axioms for DA, D_i: D_iϕ↔K_iϕ,

INCL(D) : D_Aϕ→D_Bϕwhenever A⊆B.

and, for eachi ∈Ag, the inference rule ϕ K_iϕ.

Exercise: derive Segerberg’s induction axiom:

IND_A :ϕ∧C_A(ϕ→K_Aϕ)→C_Aϕ;

V Goranko

Multi-agent Epistemic Logic: some technical results

IThe axiom system of theKC-fragment ofMAEL_n is complete.

Satisfiability/validity inMAEL^KC_n is decidable.

Adding common knowledge, however, increases the complexity, from PSPACE-complete forS5_n to EXPTIME-complete.

IThe axiom systemMAEL^KD_n of the KD-fragment of MAEL is sound and complete. MAEL^KD_n is decidable, EXPTIME-complete.

IThe full axiom systemMAEL_n is sound and complete.

MAEL_nis decidable, EXPTIME-complete.

V Goranko

Tableau based decision procedures for multi-agent epistemic logics

IV. Goranko and D. Shkatov:

Tableau-based decision procedure for the multi-agent epistemic logic with operators of common and distributed knowledge:

http://arxiv.org/abs/0808.4133

IRecently implemented by Thomas Vestergaard and available online:

http://www.thomaslyngby.dk/thesis/

IV. Goranko and D. Shkatov. Tableau-based Procedure for Deciding Satisfiability in the Full Coalitional Multi-agent Epistemic Logic: http://arxiv.org/abs/0902.2125

Waiting for implementation!

V Goranko

Exercises on multi-agent epistemic logics:

the three cards scenario revisited

Construct a Kripke model describing the three cards scenario.

Take as states all possible distributions of the cards.

Construct the update of that model after person 1 privately tells person 2 that he holds the Ace.

Find epistemic formulae, that are false in the original model but become true in the updated one, after the announcement of 1.

Using the updated model, argue that, after the announcement of person 1, person 3 still does not know the card of person 2.