• Ingen resultater fundet

# Epistemic logics: an introduction

N/A
N/A
Info
Protected

Del "Epistemic logics: an introduction"

Copied!
25
0
0

Indlæser.... (se fuldtekst nu)

Hele teksten

(1)

V Goranko

## Epistemic logics: an introduction

Valentin Goranko Technical University of Denmark

DTU Informatics

November 2010

(2)

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.

(3)

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.

(4)

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.

RW2 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 statess1 and s2. In other words, at the state s1 the agent considerss2 equally possible to be the case.

(5)

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.

(6)

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,s3 |=q∧ ¬p∧ ¬Kq∧ ¬K¬p∧K(¬Kq∧ ¬K¬p).

(7)

V Goranko

## Epistemic models: example 2

See Pacuit’s slides.

(8)

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.

KAp: “Ann knows that p”.

KBp: “Bob knows that p”.

KAKBp: “Ann knows that Bob knows that p”.

KABp:=KAp∧KBp: “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”.

(9)

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.

Kiϕ: ‘The agenti knows thatϕ’.

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

DAϕ: ‘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 ϕ’.

(10)

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.

(11)

V Goranko

## Multi-agent epistemic operators: common knowledge

Intuitively,ϕis a common knowledge amongst the agents inAif KAϕholds, andKAKAϕholds, and KAKAKAϕholds, etc. – infinitely!

This cannot be reduced to a finite chain.

Example: the coordinated attack problem.

(12)

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?

(13)

V Goranko

## The muddy children problem

See Pacuit’s slides.

(14)

V Goranko

## Multi-agent epistemic logic (MAEL): formal syntax

Formal syntax:

ϕ:=p| ¬ϕ|ϕ∨ψ|Kiϕ|KAϕ|CAϕ|DAϕ, 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.

(15)

V Goranko

## expressing some epistemic properties

ICompare: ¬K1ϕ and K1¬ϕ

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

K1ϕ→ ¬K1¬ϕ

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

K2(¬K1ϕ∧ ¬K1¬ϕ) 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 ¬K1ϕ∧ ¬K2ϕ∧C{1,2}(¬K1ϕ∧ ¬K2ϕ)∧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”.

(16)

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:

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

IP1,A∨P2,A∨P3,A; P1,A∨P1,K ∨P1,Q;

IK{1,2,3}(P1,A∨P2,A∨P3,A); K{1,2,3}(P1,A∨P1,K ∨P1,Q);

IC{1,2,3}(P1,A∨P2,A∨P3,A); C{1,2,3}(P1,A∨P1,K ∨P1,Q);

IPi,A →KiPi,A; C{1,2,3}(Pi,A →KiPi,A); ¬Pi,A →Ki¬Pi,A; IP1,A →K1¬P2,A∧ ¬K1P2,K ∧ ¬K1P2,Q;

ID{1,2}P3,A∨D{1,2}P3,K ∨D{1,2}P3,Q; IC{1,2,3}(P1,A∧P2,K →D{1,2}P3,Q).

(17)

V Goranko

## Multi-agent epistemic logic: Kripke models

Multi-agent epistemic model:

M=hS,Π, π,Ag,∼1, ...,∼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,

1, ...,∼n – the epistemic indistinguishability relations associated with the agents.

(18)

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,∼1, ...,∼ni is given by the clauses:

(Ki) M,q |=Kiϕ iff M,q0|=ϕ for allq0 such that q∼iq0.

(KA) M,q |=KAϕiff M,q0 |=ϕfor all q0 such thatq ∼EA q0, where∼EA=S

i∈Ai.

(CA) M,q |=CAϕiff M,q0 |=ϕfor all q0 such thatq ∼CA q0, where∼CA is the transitive closure of ∼EA.

(DA) M,q |=DAϕiff M,q0 |=ϕfor all q0 such that q ∼DA q0, where∼DA=T

i∈Ai.

(19)

V Goranko

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.

(20)

V Goranko

## Modeling and solving the muddy children problem

See Pacuit’s slides.

(21)

V Goranko

## Axioms for the basic multi-agent epistemic logic S5

n

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

The axioms ofS5n:

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

Inference rules: for each i:

ϕ Kiϕ.

(22)

V Goranko

## Axioms for common and distributed knowledge

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

IThe axioms forKA: KAϕ↔V

i∈AKiϕ;

I(Least) fixed point axioms forCA:

LFPA : CAϕ↔(ϕ∧KACAϕ), I Axioms forDA:

S5(DA) : The S5 axioms for DA, Di: Diϕ↔Kiϕ,

INCL(D) : DAϕ→DBϕwhenever A⊆B.

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

Exercise: derive Segerberg’s induction axiom:

INDA :ϕ∧CA(ϕ→KAϕ)→CAϕ;

(23)

V Goranko

## Multi-agent Epistemic Logic: some technical results

IThe axiom system of theKC-fragment ofMAELn is complete.

Satisfiability/validity inMAELKCn is decidable.

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

IThe axiom systemMAELKDn of the KD-fragment of MAEL is sound and complete. MAELKDn is decidable, EXPTIME-complete.

IThe full axiom systemMAELn is sound and complete.

MAELnis decidable, EXPTIME-complete.

(24)

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!

(25)

V Goranko

## 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.

Referencer

RELATEREDE DOKUMENTER

Most specific to our sample, in 2006, there were about 40% of long-term individuals who after the termination of the subsidised contract in small firms were employed on

A cancellative semigroup which satisfies a non-balanced semigroup identity has to satisfy an identity of the type x n ≡ x which implies that the semigroup is a group (of a

Until now I have argued that music can be felt as a social relation, that it can create a pressure for adjustment, that this adjustment can take form as gifts, placing the

We found large effects on the mental health of student teachers in terms of stress reduction, reduction of symptoms of anxiety and depression, and improvement in well-being

the right rule corresponds to a node where the proponent states ϕ in a defense, and the strategy has a branch for each possible opponent attack on ϕ. The left rule corresponds to a

In a series of lectures, selected and published in Violence and Civility: At the Limits of Political Philosophy (2015), the French philosopher Étienne Balibar

Copyright and moral rights for the publications made accessible in the public portal are retained by the authors and/or other copyright owners and it is a condition of

In addition, Copenhagen Business School’s Center for Shipping Economics and Innovation (CENSEI) in collaboration with the Logistics/Supply Chain Management research