Modal Logics

Connections

Related to: Non-monotonic logic
Prerequisites: Formal Systems, Classical
Requisite for: Tableau rules, Temporal Logic

Modal logics are designed to express possibility, necessity, belief, knowledge, temporal progression and other modalities. It is customary to add the operator [] with the interpretation determined by the logic. A second operator 〈〉 is the dual of the first i.e. 〈〉A = ¬[]¬A and []A = ¬〈〉¬A. Figure 1 illustrates some readings of the formulas []A and 〈〉A.

Figure 1: **Reading of []A and `〈〉`A**
	[] A		`〈〉`A
Necessity	A is necessary.	Possibly	A is possible.
Belief	A is believed.
Knowledge	A is known.
Time	A is always true.	Eventually	A is eventually true.

There are modal logics that can be used to express ideas such as:

It might rain tonight.
Life is unfair.
Mary believes that John loves her.
I know that you know that I know that you know I will be leaving town tomorrow.
He went to town for some supplies, is now carving a duck, and when he is finished, he will paint it.

The concept of necessity can be understood in several different contexts:

Logical necessity: logic requires it to be so. if A and A->B are true , then B must be true.
Epistemic necessity: reality requires it to be so. What goes up must come down.
Moral necessity: morality requires it to be so. Sinners will be punished.
Temporal necessity: Since Camile was born in 1985, she must be at least 14 years old.

Propositional modal logics provide some of the expressive power of both first and second order logic and find applications in

Artificial intelligence research area such as
- natural language translation and
- reasoning systems dealing with theories of knowledge, belief, and time.
Database systems
Software engineering
- Program specification
- Program verification
- Protocol specification
Theories of program behavior
- Algorithmic logic
- dynamic logic
- process logic
- temporal logic

Temporal logic plays an important role in the specification, derivation, and verification of programs as programs may be viewed as progressing through a sequence of states, a new state after each event in the system.

The key notion in the semantics of modal logic is the notion of possible worlds.

Syntax

Symbols and Formulas:

C = { ⊥, Τ} The propositional constants.
L = { p₀, p₁, p₂, ...} The propositional letters.
P in C union L
F ::= P | ¬F | ∧FF | ∨FF | →FF | []F | <>F {The set of formulas}

Axioms and Inference Rules:

A, A→B

The inference rule, A & B are formulas

Additional information on syntax is available.

Semantics - Multiple Worlds (Saul Kripke)

Multiple structures can be used to model modal formulas.

Figure 3: **Multiple world structure** U = **(W, A)**
A set of relational structures:	W = {w \| w is a relational structure}
An accessibility relation:	Aa subset of W×W

The set of constants in each world is monotonic in the accessibility relation however, the worlds may differ in the atomic formulas that hold for each world. U is a graph whose edges are labeled with literal formulas (the formulas required to be true by the valuation function). A model M = (W, A, w, v) is a Kripke structure. A Kripke structure where |W| = 1 corresponds to traditional logics. A reachability relation that is symmetric (Axy implies Ayx) implies that the graph is nondirectional. A reachability relation that is transitive (Axy and Ayz implies Axz) can be used to model temporal phenomenon. A reachability relation that is reflexive (Axx), symmetric, and transitive, can be used to reason about finite state systems.

The propositional modal logics share with classical propositional logic the finite model property; if a collection of formulas is satisfiable, it is satisfiable in a finite graph.

There are many modal logics. The table that follows illustrates the approach to semantics for modal logics.

Figure 4: **Model - M** |=F
where M = (U, w, v)
M\|=⊥	iff v(⊥) = false
M\|=Τ	iff v(Τ) = true
M\|= p	iff v(p) in w
M\|= ¬A	iff not M \|= A
M\|= →AB	iff M \|= ¬A or M \|= B
M\|= ¬`→`AB	iff M \|= A and M \|= ¬B
M\|= []A	iff M' \|= A for all u such that *Awu* and M' = (U, u, v)
*M \|= `<>`*A	iff M' \|= A for some u such that *Awu* and M' = (U, u, v)
M\|= ∀x.F	iff M \|= [F]^x_c for all c in C
M\|= ¬∃x.F	iff M \|= [¬F]^x_c for some c in C

A formula F is valid (a tautology), |= F, iff for all w in W, M|= F i.e., F is true in all possible worlds.

A formula F is said to be valid ( |=F ) iff it is valid in all models M (M |= F for all M). A valid formula is called a tautology. Predicate Logic (or Predicate Calculus or First-Order Logic) is a generalization of Propositional Logic. Generalization requires the introduction of variables.

Linear time temporal logic is an example of a logic that uses multiple world semantics. Each time increment is represented by a world. The accessibility relation is reflexive and transitive but not symmetric as we assume that time does not run backwards. For the formula []A, A holds in the current world and in all future worlds and for the formula <>A, A holds in either the current world or some future world.

Program specifications in temporal logic:

Safety properties: []P
Liveness properties: <>P
Safe-livenes property: [](A→<>B)
The end of time: ¬[]<>A

Additional temporal operators include

OP - next time
PUQ - P until Q

Definition

A sentence S of L is valid, |=S, if it is true in all structures for L.
A sentence S of L is a logical consequence of a set of sentences Ss of L (Ss |= S), if S is true in every structure in which all of the members of Ss are true.
A set of sentences Ss, is satisfiable if there is a structure A in which all of the members of Ss are true. Such a structure is called a model of Ss. If Ss has no model, it is unsatisfiable.

Proofs in classical logic concern truth in a single state while proofs in modal logics may involve several states. Since a formula may refer to a state other than the one in which it appears, once the collection of states has been constructed, the states must be checked to determine that all such references are satisfied.

Tableau rules for modal logic are available.
An implementation for propositional modal logic is available.
An implementation for first-order modal logic is available.

Proof Theory

In classical logic, the idea was to systematically search for a structure agreeing with the starting sentences. The result being that we get such a structure or each possible analysis leads to a contradiction. In modal logic, we try to build a frame agreeing with the sentences or see that all attempts lead to contradictions.

The Accessibility Relation

Gore 1992 has a wonderful list of axioms, a naming scheme

Figure : **Model operators and the accessibility relation**
M\|= []A	iff M' \|= A for all u such that *Awu* and M' = (U, u, v)
*M \|= `<>`*A	iff M' \|= A for some u such that *Awu* and M' = (U, u, v)


Property	Axiom	Tableau rule
reflexive	T:[]A => A
symmetric	B:A => []`<>`A
transitive	4:[]A => [][]A
serial	D:[]A => `<>`A

Temporal logic and the Next time operator
	Formula		Recursive definition
Always A	[]A	=	A /\ 0[]A
Eventually A	`<>`A	=	A \/ 0`<>`A
A Until B	A U B	=	B \/ (A /\ 0(A U B))

Models

K(ripke) - minimal modal logic

Axioms

All propositional tautologies
[](p->q) -> ([]p->[]q)

Rules of inference

from p and p->q, infer q.

A theorem prover for K is available.

B - self knowledge and knowledge of falsehoods

reflexive and symmetric

Axioms

All propositional tautologies
[]p→p (reflexivity)
[](p→q) → ([]p→[]q)
[]p→[][]p (transitivity)

The accessibility relation must be reflexive and transitive.

Rules of inference

from p and p→q, infer q.
from p, infer []p.

D, D4, K, K4, K5, KB

T - knowledge is true belief

reflexive

M

Axioms

All propositional tautologies
[]p→p (reflexivity)
[](p→q) → ([]p→[]q)

Rules of inference

from p and p→q, infer q
from p, infer []p

S4 - positive self reflection

reflexive and transitive

Axioms

All propositional tautologies
[]p -> p
[](p->q) -> ([]p->[]q)
[]p ->[][]p

Rules of Inference

from p and p->q, infer q
from p, infer []p

S5, E - knowledge of non-knowledge (complete awareness)

reflexive, symmetric, & transitive

Axioms

All propositional tautologies
[]p -> p
[](p->q) -> ([]p->[]q)
[]p ->[][]p
<>p -> []<>p

Rules of Inference

from p and p->q, infer q
from p, infer []p

Belief, Knowledge and Self-Awareness

What kind of logic allows us to reason about our set of beliefs and our own self-awareness?

Connections

Related to: Modal
Prerequisites: Formal Systems, Classical
Requisite for:

The following is adapted from Raymond Smullyan's book Forever Undecided.

Reasoning about beliefs requires a set of beliefs and a logic. The following is a description of a propositional belief logic based on propositional logic extended with the symbol B; BX is read `believes X' with the meaning that X is in the set of beliefs (See Figure N.1 and N.2).

Figure 1: **Syntax**
Symbols and Formulas: L = { p₀, p₁, p₂, ...} The propositional letters. P in L F ::= P \| ¬F \| `->`FF \| BF {The set of formulas}

The syntax was chosen to avoid the use of parentheses. Informally, we use the more common infix notation and additional logical operators.

Conjunction: (A /\ B) = ¬->A¬B
Disjunction: (A \/ B) = ->¬AB
Biconditional: (A<->B) = (->AB) /\ (->BA) = (/\AB) \/ (/\¬A¬B)
Conditional: (A->B) = ->AB

The semantics of Belief Logic include a set of beliefs and extend the valuation function of propositional logic to formulas containing the belief operator. Since beliefs are collections of formulas, we map a formula to true iff it is in the list of beliefs (See Figure N.2).

Structure and Interpretation. <SB, v>

false

true

->

A function v is a valuation function if it is a total
function on L and with the structure <v, SB> satisfies
the following properties:

<SB, v> \|= P	iff	v(P) = true
<SB, v> \|= ¬P	iff	v(P) = false
<SB, v> \|= ¬¬A	iff	<SB, v> \|= A
<SB, v> \|= ¬`->`AB	iff	<SB, v> \|= A and <SB, v> \|= ¬B
<SB, v> \|= `->`AB	iff	<SB, v> \|= ¬A or <SB, v> \|= B
<SB, v> \|= B A	iff	SB \|= A
<SB, v> \|= ¬B A	iff	SB \|= ¬A

A formula F is satisfiable iff it is true under some valuation function v and a set of beliefs SB, i.e., <v, SB> |= F. A formula F is a tautology iff it is true under all valuation functions. A tautology is said to be valid and is written |= F.

Figure 6: **Proof theory: inference**
Axioms	A the tautologies
Rule of inference: Modus Ponens	A and A`->`B B

A set of formulas is said to be logically closed iff it contains all tautologies and is closed under modus ponens (for any formulas A and B, if A and ->AB are in the set, then so is B).

A logically closed set of formulas is said to be inconsistent iff it contains both a formula and its negation, i.e., there is a formula A in the set such that both A and ¬A are in the set. Equivalently, a set of formulas is said to be inconsistent iff it contains all formulas. A logically closed set of formulas is said to be consistent if it is not inconsistent.

Theorem: Prove that the two definitions of inconsistent are equivalent.
Proof: Clearly, the second definition implies the first. So, let F be a logically closed set of formulas that contains A and ¬A. Let Q be an arbitrary formula. The formulas, A->¬A->A/\¬A, and A/\¬A->Q, are tautologies and so are in F. By three applications of MP, Q is in F.

Definitions

A reasoner is called accurate if for any proposition A, if (s)he believes A, then A is true; BA->A A reasoner is called inaccurate if for some proposition A, if (s)he believes A, then ¬A is true. BA->¬A A reasoner is called consistent if the set of all propositions the (s)he believes is a consistent set. ¬(BA /\ B¬A) A reasoner is called normal if for any proposition P, if (s)he believes A, then (s)he believes that (s)he believes A. BA -> BBA A reasoner is called peculiar if for some proposition A, (s)he believes A and (s)he believes that (s)he doesn't believe A. BA /\ B¬BA A reasoner is called regular if for any propositions A and B, if (s)he believes A->B, then (s)he also believes (BA->BB). B(A->B)->B(BA->BB)

Observations: A reasoner believes that (s)he is consistent if for all formulas, A, (s)he believesB¬B(A/\¬A). A reasoner believes that (s)he is inconsistent if for some formula A, (s)he believes BB(A/\¬A).

Advancing stages of self-awareness

What does it mean for an individual to be self-aware? People are aware of some external and internal events (their thoughts) and are able to recognize their image. They are not aware of their atoms. We interpret the operator B to mean aware of.

Formula	Means
BA	I am aware of A
BBA	I am aware of my beliefs.
*BBB*A	I am aware that I am aware of my beliefs

Now we define several types of reasoners.

A reasoner is of type 0 if the set of beliefs are the tautologies.
1. (S)he believes all tautologies, i.e., if |=X (X is a tautology), then <v, SB> |=BX.

A reasoner is of type 1 if the reasoner is of type 0 and the set of the reasoner's beliefs are logically closed i.e.,

If (s)he believes A and believes A->B then (s)he believes B i.e.,

from infer

<SB, v> |=BA and <SB, v> |=B(A->B)

<SB, v> |=BB

A reasoner is of type 2 if the reasoner is of type 1 and believes that her/his set of beliefs is logically closed i.e.,

<SB, v> |=B((BA /\ B(A->B))->BB)

A reasoner is of type 3 if the reasoner is of type 2 and is aware of her/his beliefs i.e.,

<SB, v> |=BA->BBA

for any formula A. Any reasoner that is aware of her/his beliefs is said to be normal.

A reasoner is of type 4 if the reasoner is of type 3 and is aware that (s)he is aware of her/his beliefs i.e.,

<SB, v> |=B(BA->BBA)

for any proposition A. A reasoner of type 4 knows that (s)he is normal.

Exercises/Theorems

Explain: Reasoners of type 2 know how they reason -- they know their inference rule.
Explain: A reasoner of type 4 knows that (s)he is normal.
Prove that every reasoner of type 3 believes the proposition: (Bp/\B¬p)->B(p/\¬p).

Proof:

->

Prove that every reasoner of type 3 is regular.
Prove that if a regular reasoner of type 1 believes BA for some proposition A then (s)he must be normal.
Prove that any peculiar normal reasoner of type 1 must be inconsistent.
Prove that every reasoner of type 4 knows that (s)he is normal.
Prove that any reasoner of type 4 knows that if (s)he should ever be peculiar, (s)he will be inconsistent.

Awareness of Self-Awareness

A reasoner believes that (s)he is of type 1 if (s)he believes all propositions of the form: BX where X is a tautology and believes all propositions of the form: (BA /\ B(A->B))->BB BBX - X is a tautology
B((BA /\ B(A->B))->BB)

A reasoner believes that (s)he is of type 2 if (s)he believes that (s)he is of type 1 and believes all propositions of the form: B((BA/\B(A->B))->BB

BBX - X is a tautology
B((BA /\ B(A->B))->BB)
BB((BA/\B(A->B))->BB)

A reasoner believes that (s)he is of type 3 if (s)he believes that (s)he is of type 2 and believes all propositions of the form: BA ->BBA

BBX - X is a tautology
B((BA /\ B(A->B))->BB)
BB((BA/\B(A->B))->BB)
B(BA -> BBA)

A reasoner believes that (s)he is of type 4 if (s)he believes that (s)he is of type 3 and believes all propositions of the form: B(BA ->BBA)

BBX - X is a tautology
B((BA /\ B(A->B))->BB)
BB((BA/\B(A->B))->BB)
B(BA -> BBA)
BB(BA -> BBA)

A reasoner knows that (s)he is of type X if (s)he is of type X and believes that (s)he is of that type.

Exercises/Theorems

Prove that if a reasoner of type 4 knows that (s)he is regular.
Prove that a reasoner of type 4 knows that (s)he is of type 4.
Prove that if a reasoner of type 4 ever believes that (s)he cannot be inconsistent, (s)he will become inconsistent.
Suppose a normal reasoner of type 1 believes a proposition of the form p<->¬Bp. Then:
1. If (s)he ever believes p, then (s)he will become inconsistent.
2. If (s)he is of type 4, then (s)he knows that if (s)he should ever believe p then (s)he will become inconsistent--i.e., (s)he will believe the proposition Bp->B_|_.
3. If (s)he is of type 4 and believes that (s)he cannot be inconsistent, then (s)he will become inconsistent.

The following is based on a paper by Halpern.

Knowledge

A logic of knowledge is used as a tool for analyzing multi-agent systems - players in a poker game, processes in a computer network, or robots on an assembly line.

We introduce three new operators:

K_iA - agent i knows A if A is true in all worlds agent i thinks possible
E_GA - each agent in the group G knows A
C_GA - A is common knowledge among the agents in the group G

Common knowledge is defined as "everyone knows A, and everyone knows that everyone knows A, and ..."

Symbols and formulas:

The propositional formulas
L = { p₀, p₁, p₂, ...}, P in L
The set of formulas
F ::= P | ¬F | ∧FF | K_iF | E_GF | C_GF

M = (S, v, K₁, ... , K_n) - A Kripke structure where

S - a set of states or possible worlds
v in S×L -> {0,1}
K_i an equivalence relation on S

(M, s) \|= p	iff	v(s,p) = 1
(M, s) \|= ¬A	iff	not (M, s) \|= A
(M, s) \|= A∧B	iff	(M, s) \|= A and (M, s) \|= B
(M, s) \|= K_iA	iff	(M, t) \|= A for all t such that (s,t) in K_i
(M, s) \|= E_GA	iff	(M, s) \|= K_iA for all i in G
(M, s) \|= C_GA	iff	(M, s) \|= *E^k_GA for k=1, 2, ..., where E¹_GA = E_GA and E^k+1*_GA = E_GE^k_GA

The following axiom system is sound and complete.

Figure : **Axioms**
A1. All propositional tautologies A2. K_iA ∧ K_i(A→B) `→`K_iB A3. K_iA `→` A A4. K_iA `→` K_iK_iA A5. ¬K_iA `→` K_i¬K_iA R1. From A and A`→`B infer B R2. From A infer K_iA C1. E_GA `→` ∀_{i in G}K_iA C2. C_GA `→` E_G(A/\CA) RC1. From A `→` E_G(A∧B) infer A `→`C_GB

A1 and R1 are a sound an complete axiom system of classical propositional logic. A2 says that an agent's knowledge is closed under implication. A3 says that an agent knows only things that are true. This axiom is usually taken to distinguish knowledge from belief i.e., false statements may be believed but not known. A4 and A5 are axioms of introspection; these are usually rejected by philosophers.

C2 (fixed point axiom) says that common knowledge of A holds exactly when everyone in the group knows A and that A is common knowledge.

Exercises

Rewrite the following in English: K₁K₂A ∧ ¬K₂K₁K₂A.
Express symbolically, Dean doesn't know whether Nixon knows that Dean knows that Nixon knows that McCord burgled O'Brien's office at Watergate. Hint: let A be the statement "McCord burgled O'Brien's office at Watergate".
Express symbolically, Everyone in G knows p, but p is not common knowledge.
Construct a model for the situation where agent 1 does not know "it is sunny in San Francisco" but agent 2 does.
Interpret axiom A4: K_iA → K_iK_iA
Interpret axiom A5: ¬K_iA → K_i¬K_iA.
Show that A3 - A5 are valid.
Show that C2 is necessary for agreement and coordination.
Show that the theory is decideable and decidability is of exponential complexity.

Multi-Agent Systems

Logical Omniscience

An agent is logically omniscient iff it knows all tautologies and its knowledge is closed under modus ponens.

What is logically knowable is not realizable in practice since real agents are resource-bounded. Attempts to define knowledge in the presence of bounds include

restricting what an agent knows to a set of formulas which is not closed either under inference or all instances of the a given axiom.
defining a set of possible worlds which in turn, defines a set of formulas.
change the logic to a non-standard logic such as relevance logic
a impossible worlds to the list of worlds
restrict the depth of Ks found in formulas
add an operator for awareness so that the formulas that an agent is aware of is a subset of the formulas. An agent knows a formula iff it is true in each possible world of the agent.
awareness can be defined to mean that an agent can use a local algorithm to compute an answer.

Future Directions

Implement a logical agent.
Reason about knowledge/belief change over time
Knowledge based programming: The goal is to allow the programmer to write a program by saying what she wants rather than painfully describing how to compute what she wants.
Analyze protocols and construct logical agents to implement the protocol
More realistic models of knowledge that incorporate resource-bounded reasoning, probability, and the possibility of errors.
A deeper understanding of the interplay between various modes of reasoning under uncertainty.

References

Halpern, Joseph Y: Reasoning about Knowledge: A Survey (1995)
Gore Rajeev Prabharkar: Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logics. (1992)
Smullyan, Raymond (1987): Forever Undecided Alfred A. Knopf Inc.
Stanford Encylopedia of Philosophy: Modal Logic
Beckert, Bernhard and Gore, Rajeev: ModLeanTAP
Advances in Modal Logic

Content licensed under OPL

Author: Anthony A. Aaby

Comments and content invited aabyan@wwc.edu

M\|=⊥	iff v(⊥) = false
M\|=Τ	iff v(Τ) = true
M\|= p	iff v(p) in w
M\|= ¬A	iff not M \|= A
M\|= →AB	iff M \|= ¬A or M \|= B
M\|= ¬`→`AB	iff M \|= A and M \|= ¬B
M\|= []A	iff M' \|= A for all u such that *Awu* and M' = (U, u, v)
*M \|= `<>`*A	iff M' \|= A for some u such that *Awu* and M' = (U, u, v)
M\|= ∀x.F	iff M \|= [F]^x_c for all c in C
M\|= ¬∃x.F	iff M \|= [¬F]^x_c for some c in C

M\|= []A	iff M' \|= A for all u such that *Awu* and M' = (U, u, v)
*M \|= `<>`*A	iff M' \|= A for some u such that *Awu* and M' = (U, u, v)