A Primer on Modal and Epistemic Logic
A self-contained reference tutorial. Work through each section in order. By the end you will have the formal machinery to read and construct modal logic proofs about Belief-Desire-Intention (BDI) agents.
Classical propositional and predicate logic are powerful tools, but they have a fundamental limitation for reasoning about AI agents: they only deal with what is true, not with what an agent believes, knows, or considers possible.
Consider these four sentences:
1. "It is raining." ← classical logic handles this fine: the statement is true or false
2. "Alice believes it is raining." ← classical logic has no operator for "believes"
3. "Bachelors are necessarily unmarried." ← classical logic has no way to distinguish necessary truth from contingent truth
4. "Bob knows that Alice believes it is raining." ← classical logic cannot express nested mental states at all
Sentences 2–4 involve modalities — ways in which something is true, or who holds it to be true. Modal logic adds the operators needed to handle them. Epistemic logic is a specialization of modal logic focused specifically on knowledge and belief.
Note on sentence 3: Classical logic can prove that "bachelors are unmarried" is true — given the definition of bachelor, it follows by logic. What it cannot express is the modal status of that truth: the distinction between something that is true as a matter of definition (could not be otherwise) versus something that happens to be true right now but could have been otherwise, like "it is raining." Modal logic adds that distinction.
An AI agent operating in the world must reason about:
Classical logic cannot express any of these distinctions. Modal and epistemic logic can.
These two terms appear throughout this tutorial, often without a clear statement of how they relate. Here it is, before anything else:
Modal logic extends classical propositional logic with two operators — □ (necessarily) and ♢ (possibly) — and a semantics based on possible worlds. It is a general-purpose framework that can be applied to many different domains depending on how you interpret "accessible world."
Examples of modal logic applied to different domains:
Epistemic logic is modal logic with a specific intended interpretation: the □ operator represents knowledge or belief, and the accessibility relation R encodes which worlds an agent considers possible given its current information.
It was developed by Jaakko Hintikka in 1962 specifically to reason formally about what agents know and believe — which is exactly what we need for the Belief-Desire-Intention (BDI) framework.
Epistemic logic inherits all the machinery of modal logic — possible worlds, accessibility relations, axioms — and adds the specific interpretation that makes □ mean "knows" or "believes," and ♢ mean "the agent considers it possible that."
Since □ and ♢ are duals (♢φ ⟺ ¬□¬φ), "the agent considers φ possible" is equivalent to "the agent does not know/believe that φ is false."
The analogy: modal logic is the engine. Epistemic logic is one vehicle built on that engine. Temporal logic, deontic logic, and dynamic logic are other vehicles built on the same engine. You need to understand the engine — possible worlds, □, ♢, accessibility relations, axioms — before the vehicle makes sense. That is why this tutorial covers modal logic first (Sections 2–4) and epistemic logic second (Section 5).
Goal of this tutorial: build the formal machinery from scratch, with every term defined before it is used, so that you can read and write modal logic proofs about belief, knowledge, and rational agency in BDI systems.
Modal logic is built on top of classical propositional logic. This section establishes the foundation. Even if you know this material, pay attention to the ⊢ vs ⊨ distinction at the end — it is commonly confused and important for modal logic proofs.
A proposition is any declarative statement that is either true or false, but not both. We use lowercase letters p, q, r or Greek letters φ (phi), ψ (psi) as placeholder names for propositions.
Connectives combine propositions to form new propositions:
| Symbol | Name | Meaning | Example (p = "raining", q = "windy") |
|---|---|---|---|
| ¬p | Negation | not p | "it is not raining" |
| p ∧ q | Conjunction | p and q — both must be true | "it is raining and windy" |
| p ∨ q | Disjunction | p or q — at least one must be true | "it is raining or windy (or both)" |
| p ⟹ q | Implication | if p then q | "if it is raining then carry an umbrella" |
| p ⟺ q | Biconditional | p if and only if q | "it is raining if and only if the ground is wet" |
The implication p ⟹ q (read "if p then q") is defined by this truth table, where p and q are specific propositions with known truth values:
The only case where p ⟹ q is false is when p is true and q is false — the condition holds but the consequence fails.
An important note — why implication is defined as ¬p ∨ q: The material conditional p ⟹ q is not taken as a primitive in classical logic. Instead it is defined as ¬p ∨ q — "not-p or q." These two expressions have identical truth tables:
Every row matches, so they are logically equivalent. The reason for defining implication this way is economy: ¬ and ∨ are more primitive operations, and by defining ⟹ in terms of them, the whole system needs fewer primitives. The cost is the vacuously true cases: when p is False, ¬p is True, so ¬p ∨ q is True regardless of q — with no meaningful connection between p and q required. Many philosophers and logicians find this unsatisfying, and alternative logics handle it differently. In classical propositional logic, accept it as a definition.
Aside — strict implication and the motivation for modal logic
The vacuous truth problem motivated C.I. Lewis in 1918 to propose strict implication as a better account of what we actually mean when we say "p implies q" in reasoning and argumentation.
Strict implication is written □(p ⟹ q) and means: in every accessible world, p ⟹ q holds. This uses the possible worlds semantics defined formally in Section 2: at world w, □(p ⟹ q) is true if and only if for every world w₁ such that wRw₁ (w₁ is accessible from w), the material conditional p ⟹ q is true in w₁.
This is substantially stronger than plain p ⟹ q. Here is why, using the same example throughout:
Let p = "it is raining" and q = "the ground is wet."
Plain p ⟹ q (material conditional, current world only): true today simply if it happens not to be raining — vacuously, with no required connection between rain and wet ground.
□(p ⟹ q) (strict implication, all accessible worlds): true only if in every world I consider possible, whenever it rains the ground is wet. This rules out any accessible world where it rains but the ground stays dry — even if the current world happens to be dry. There is no escape through a false antecedent in a world where the antecedent holds.
Strict implication expresses a law-like necessary connection rather than a coincidental truth, and it is one of the principal historical motivations for developing modal logic. The □ operator gives us a way to say not just that something is true, but that it holds necessarily — across all situations we consider possible. This distinction between what happens to be true and what must be true runs through everything in Sections 2–7 of this tutorial.
Note: strict implication has its own problems (the "paradoxes of strict implication"), which is why relevance logic and intuitionistic logic were developed as further alternatives. But for the purposes of this tutorial, strict implication is the key stepping stone from classical logic into modal logic.
Given true premises, inference rules produce new true conclusions. The two most important:
Example: "If it rains, carry an umbrella" + "It is raining" → "Carry an umbrella."
Example: "If it rains, ground is wet" + "Ground is not wet" → "It is not raining."
These symbols look similar but mean different things. Confusing them is one of the most common errors in logic proofs.
Γ is a set of propositions — a collection of statements treated as premises or assumptions. For example, Γ = {p, p⟹q, q⟹r} is a set of three propositions. Saying "all of Γ is true" means every proposition in the set is true simultaneously in the same situation.
φ can be derived from Γ by applying inference rules. A formal proof exists. This is purely about symbol manipulation — no interpretation required.
Read as: "φ is provable from Γ."
φ is true in every assignment of truth values to propositions that makes all of Γ true. This is about meaning and truth, not symbol manipulation.
Read as: "φ is true in every assignment of truth values to propositions that makes all of Γ true" or "Γ logically implies φ."
A logical system is sound if Γ ⊢ φ guarantees Γ ⊨ φ — every provable statement is true. It is complete if Γ ⊨ φ guarantees Γ ⊢ φ — every true statement is provable. Classical propositional logic is both sound and complete.
Aside — Gödel's incompleteness theorems
We just said classical propositional logic is both sound and complete. This is a genuine theorem — but it only holds because propositional logic is a relatively weak system. For stronger systems, completeness breaks down in a fundamental way.
Gödel's First Incompleteness Theorem (1931): Any formal system that is (a) consistent — it cannot prove both φ and ¬φ — and (b) expressive enough to encode basic arithmetic, contains statements that are true but cannot be proved within that system.
In other words: for sufficiently powerful systems, Γ ⊨ φ does not guarantee Γ ⊢ φ. There exist true statements that no proof can reach.
Why propositional logic escapes this: Gödel's theorem requires the system to be expressive enough to talk about arithmetic — natural numbers, addition, multiplication. Propositional logic has no quantifiers and no variables ranging over numbers, so it cannot encode arithmetic at all. It is too weak to be caught by incompleteness. First-order predicate logic over arithmetic is where the theorem bites.
Gödel's Completeness Theorem (1929): One year before the incompleteness theorem, Gödel proved that first-order predicate logic itself — without arithmetic — is complete: every semantically valid formula is provable. The incompleteness appears when you add the axioms of arithmetic on top.
Connection to Section 6: Gödel's theorem gives a second, deeper reason why logical omniscience is unrealistic. Standard epistemic logic assumes agents know all consequences of their beliefs. But if an agent's beliefs include arithmetic, Gödel guarantees there are true consequences that are unprovable — no finite derivation can reach them. Konolige's bounded deduction model (Section 6) sidesteps both problems at once: by restricting to a finite rule set r, the agent is neither expected to know all consequences nor capable of deriving unprovable truths.
Before introducing the modal operators □ and ♢, we need a precise account of what they mean — a semantics. The standard semantics, developed by Saul Kripke in 1963, is called possible worlds semantics. All modal logic terminology is defined here, before it is used anywhere else in this tutorial.
A possible world is a complete, consistent assignment of truth values to every proposition in the vocabulary under consideration — the fixed set of propositions relevant to the problem at hand. It describes one complete way things could be within that vocabulary. We use lowercase letters w, w₁, w₂, w' to name individual worlds. The actual world is the world that corresponds to reality as it currently is.
Think of a possible world as a row in a giant truth table — one that assigns True or False to every proposition simultaneously. The actual world is the row that matches reality right now. Other rows are other ways things could have been, or could be.
A Kripke model M is a triple M = (W, R, V) consisting of three components defined below.
Let p = "it is raining" and q = "Alice is carrying an umbrella."
In the actual world w₀: it is raining (p = True) and Alice is not carrying an umbrella (q = False). Alice is indoors and cannot see outside, so she does not know whether it is raining. Because she lacks this information, she considers two worlds possible from w₀ — one in which it is raining and one in which it is not:
The arrows represent the accessibility relation R. Here w₀Rw₁ and w₀Rw₂ — Alice considers both w₁ and w₂ possible from her current position in w₀.
We write M, w ⊨ φ to mean "formula φ is true in model M at world w." For classical connectives, truth is evaluated within each world exactly as in propositional logic. For modal operators:
M, w ⊨ □φ if and only if for every world w₁ such that wRw₁, M, w₁ ⊨ φ.
That is: φ is true in every world accessible from w.
M, w ⊨ ♢φ if and only if there exists a world w₁ such that wRw₁ and M, w₁ ⊨ φ.
That is: φ is true in at least one world accessible from w.
Applying these definitions to the Alice example. Notice the important distinction: the actual world w₀ tells us what is really true (it is raining, no umbrella), while the accessible worlds w₁ and w₂ represent what Alice considers possible given her limited information. Modal operators □ and ♢ range over the accessible worlds, not the actual world directly.
A formula φ is valid, written ⊨ φ, if it is true at every world in every possible Kripke model. A valid formula is a tautology of modal logic — it holds no matter what. This is a much stronger claim than being true at one particular world in one particular model.
Now that possible worlds and the accessibility relation R are defined, we can give the modal operators □ and ♢ their full formal treatment. Their semantics were defined in Section 2. This section covers their syntax, their relationship to each other, and how they compose.
□φ is true at world w if φ is true in every world w₁ such that wRw₁ — every world accessible from w.
Read as: "necessarily φ" or "in all accessible worlds, φ."
♢φ is true at world w if there exists at least one world w₁ such that wRw₁ and φ is true in w₁.
Read as: "possibly φ" or "in some accessible world, φ."
□ and ♢ are defined in terms of each other, just as ∀ (for all) and ∃ (there exists) are duals in predicate logic:
The analogy with quantifiers: □ behaves like ∀ (quantifying over all accessible worlds) and ♢ behaves like ∃ (quantifying over at least one accessible world). Just as ∀x P(x) ⟺ ¬∃x ¬P(x), we have □φ ⟺ ¬♢¬φ.
Let p = "the door is locked" and q = "the key is needed."
Modal operators can be nested. To understand what □□φ means, we need to trace through two steps of the accessibility relation.
Recall: wRw₁ means "world w₁ is accessible from world w" — there is a directed arrow from w to w₁ in the graph.
□□φ is true at world w if and only if: for every world w₁ such that wRw₁, and for every world w₂ such that w₁Rw₂, φ is true in w₂.
In graph terms: φ holds at every world reachable from w via any intermediate world w₁ along arrows of R.
To understand why □□φ is a non-trivial claim, we need to understand what it means for R to be transitive — and what happens when it is not.
The accessibility relation R is transitive if whenever (w, w₁) ∈ R and (w₁, w₂) ∈ R, it follows that (w, w₂) ∈ R.
In graph terms: if there is an arrow from w to w₁ and an arrow from w₁ to w₂, then there is also a direct arrow from w to w₂.
Transitivity says: anything reachable in two steps is also reachable in one step directly.
If R is not transitive, there can exist worlds w, w₁, w₂ such that (w, w₁) ∈ R and (w₁, w₂) ∈ R but (w, w₂) ∉ R — w₂ is reachable from w by going through w₁, but there is no direct arrow from w to w₂.
Example — non-transitivity with Alice, Bob, and Carol
Imagine three people: Alice, Bob, and Carol. Alice can see Bob's computer screen. Bob can see Carol's computer screen. Alice cannot see Carol's screen directly.
Model this as three worlds representing what each person knows:
The accessibility relation R contains: (w, w₁) and (w₁, w₂). But it does not contain (w, w₂) — Alice has no direct view of Carol's screen, so Alice does not consider Carol's world directly accessible.
R is not transitive in this model.
Now consider what □φ and □□φ mean at w:
□φ at w: φ holds in every world directly accessible from w. The only directly accessible world is w₁ (Bob's world). So □φ says: φ is true in Bob's world. It says nothing about Carol's world w₂, because (w, w₂) ∉ R.
□□φ at w: in every world directly accessible from w (that is, w₁), φ holds in every world directly accessible from w₁ (that is, w₂). So □□φ requires φ to be true in Carol's world w₂.
In this non-transitive model, □φ and □□φ are genuinely different claims. □φ covers worlds one arrow away (w₁ only). □□φ covers worlds two arrows away (w₂ via w₁). Alice knowing something (□φ) does not imply Alice knowing that Bob knows it (□□φ), because Alice cannot see what Bob sees about Carol.
If R were transitive: the direct arrow (w, w₂) would exist. Then w₂ would already be in the set of worlds directly accessible from w, and □φ would already require φ to hold in w₂. The two-step and one-step accessible worlds would coincide, and □□φ would add nothing beyond □φ — they would be equivalent.
Axiom 4 (□φ ⟹ □□φ) is precisely the axiom that forces R to be transitive. By adopting Axiom 4, you are asserting: there are no two-step paths that are not also one-step paths. Every w₂ reachable in two steps is also reachable in one step directly. In agent terms: if an agent believes φ (in all worlds it can reach), then it also believes that it believes φ (φ holds in all worlds reachable from those worlds) — because transitivity collapses the two levels into one.
The semantic meaning of □ and ♢ depends on the structure of the accessibility relation R. Different constraints on R give different valid formulas — these formulas are the axioms of the modal system. Adding axioms restricts which Kripke models are allowed.
Every modal logic includes at minimum two rules:
What the necessitation rule does and does not allow
The necessitation rule applies only to logical tautologies — formulas that are true in every world in every possible model, regardless of how propositions are interpreted. It does not apply to propositions that merely happen to be true in the current world.
A logical tautology is a formula whose truth depends only on its logical structure, not on what the propositions mean. Examples:
The necessitation rule allows us to conclude □(p ∨ ¬p) — "necessarily, either p or not-p." This is valid because p ∨ ¬p holds in every world in every model.
Now contrast this with a contingent truth — a proposition that happens to be true in the current world but is not guaranteed to be true in every world. Let p = "it is raining." Suppose it is raining right now, so p is true in the current world w. The necessitation rule does not allow us to conclude □p — "necessarily, it is raining." That would be absurd: it might not be raining in other accessible worlds, and probably is not raining in all of them.
The distinction in a single sentence: the necessitation rule licenses moving from logical necessity (true in every world in every model) to □, but not from contingent truth (true in this world right now) to □. Conflating these two is one of the most common errors when first working with modal logic.
These two rules alone define system K. They are necessary but not sufficient for reasoning about agent beliefs. We add further axioms for that.
| Name | Formula | Plain English | Constraint on R |
|---|---|---|---|
| T Truth axiom |
□φ ⟹ φ | If φ is true in all accessible worlds, then φ is true in the current world. | R must be reflexive: for every world w, wRw. Every world is accessible from itself. |
| 4 Positive introspection |
□φ ⟹ □□φ | If φ holds in all worlds accessible from w, then φ also holds in all worlds accessible from those worlds. | R must be transitive: if wRw₁ and w₁Rw₂ then wRw₂. Two-step paths are also one-step paths. |
| 5 Negative introspection |
¬□φ ⟹ □¬□φ |
¬□φ means: there exists at least one accessible world w₁ in which φ is false. □¬□φ means: in every accessible world w₁, there exists at least one world accessible from w₁ in which φ is false. The axiom says: if the agent does not believe φ, then in every world the agent considers possible, that non-belief persists. In agent terms: the agent is aware of its own non-beliefs. This is called negative introspection. |
R must be Euclidean: if wRw₁ and wRw₂ then w₁Rw₂. |
| D Consistency |
□φ ⟹ ♢φ | If φ holds in all accessible worlds, then φ holds in at least one accessible world. Necessary things are possible. |
R must have the following property: for every world w in W, there exists at least one world w₁ in W such that wRw₁ — every world has at least one accessible world. R never dead-ends. This property is called serial in the mathematical literature — the relation continues indefinitely, with no world from which all paths stop. The practical meaning for agents: the agent always has at least one world it considers possible. Without this, an agent could have no accessible worlds at all, making □φ vacuously true for every φ simultaneously — including contradictions — making the belief system inconsistent. |
Axiom T states: □φ ⟹ φ. In semantic terms: if φ is true in every world accessible from w, then φ is true in w itself. This requires w to be accessible from itself — i.e., wRw.
Because wRw, world w is in its own set of accessible worlds. So "φ is true in all accessible worlds" includes "φ is true in w." Therefore □φ ⟹ φ holds. Without the self-loop, the current world might not be accessible from itself, and □φ could hold even if φ is false in w.
Axiom 4 states: □φ ⟹ □□φ.
Recall from Section 3: □□φ at world w means φ holds in every world w₂ reachable from w in two steps — i.e., every w₂ such that there exists w₁ with wRw₁ and w₁Rw₂.
Axiom 4 says: if φ holds in every world one step from w, then φ also holds in every world two steps from w. This is automatically true when R is transitive — because if wRw₁ and w₁Rw₂, transitivity gives wRw₂ directly, so w₂ is already among the one-step accessible worlds where φ holds.
For agents: Axiom 4 means that if an agent believes φ (□φ), then the agent believes that it believes φ (□□φ). This is called positive introspection — the agent is aware of its own beliefs. It is essential for reasoning about the stability of intentions across accessible worlds, as we will see in Section 7.
Named modal logic systems follow a simple convention: the name lists the axioms added on top of the base system K. Each letter corresponds to one axiom:
The standard systems used in this tutorial are:
As introduced in Section 0, epistemic logic is modal logic with a specific interpretation: the □ operator represents knowledge or belief, and the accessibility relation R encodes which worlds an agent considers possible given its information. It was developed by Jaakko Hintikka in 1962 and is the standard formal tool for reasoning about what agents know and believe. Everything from Sections 2–4 — possible worlds, the accessibility relation R, the operators □ and ♢, and the axioms — carries over directly. What changes is only the interpretation we give to those structures.
The epistemic accessibility relation for agent i, written Rᵢᴷ, is the set of ordered pairs (w, w₁) such that agent i considers world w₁ possible from world w — given everything the agent knows. World w₁ is epistemically accessible from w for agent i if agent i cannot rule out w₁ based on its knowledge in w.
The epistemic accessibility relation satisfies Axiom T (it is reflexive: wRᵢᴷw for all w), which ensures that what the agent knows is actually true. It typically also satisfies Axioms 4 and 5, giving the full KT45 system for knowledge (also called S5 in the literature).
The doxastic accessibility relation for agent i, written Rᵢᴮ, is the set of ordered pairs (w, w₁) such that agent i considers world w₁ possible from world w — given what the agent believes. World w₁ is doxastically accessible from w for agent i if world w₁ is consistent with the agent's beliefs in w.
The doxastic accessibility relation does not require Axiom T (it need not be reflexive). This means the actual world w need not be among the worlds the agent considers possible — the agent can hold false beliefs. It typically satisfies Axioms 4 and 5 but not T, giving the KD45 system for belief.
Both terms trace to ancient Greek, and the distinction between them maps precisely onto the formal distinction between knowledge and belief in epistemic logic:
The formal properties of the two accessibility relations in epistemic logic directly reflect this ancient philosophical distinction: the epistemic relation satisfies Axiom T (what is known is true — episteme is factive), while the doxastic relation does not (what is believed may be false — doxa is not factive).
Kᵢφ is true at world w if φ is true in every world w₁ such that wRᵢᴷw₁, where Rᵢᴷ is the epistemic accessibility relation for agent i — the worlds agent i cannot rule out given its knowledge.
Because Rᵢᴷ satisfies Axiom T (reflexive), Kᵢφ ⟹ φ: what the agent knows is actually true in the current world.
Bᵢφ is true at world w if φ is true in every world w₁ such that wRᵢᴮw₁, where Rᵢᴮ is the doxastic accessibility relation for agent i — the worlds consistent with the agent's beliefs.
Because Rᵢᴮ does not require Axiom T (not necessarily reflexive), Bᵢφ does not imply φ: the agent can believe false things. The actual world w need not be among the worlds the agent considers possible.
You believed it would be sunny today. It rained. Your belief was false — but it was still a genuine belief. If you had known it would be sunny, it would have been sunny. Knowledge is factive (truth-guaranteeing); belief is not.
In a multi-agent system with agents 1, 2, ..., n, each agent i has its own accessibility relation — Rᵢᴷ for knowledge or Rᵢᴮ for belief — on the set of worlds W. The relation encodes which worlds agent i considers possible from each world.
The pair (w, w₁) is in agent i's epistemic accessibility relation Rᵢᴷ (or doxastic relation Rᵢᴮ). Read as: "from world w, agent i considers world w₁ possible given its knowledge (or beliefs)." In graph terms: there is a directed arrow labelled i from node w to node w₁. The superscript K or B indicates whether the relation encodes knowledge or belief.
Two agents in the same world can have completely different accessibility relations — they may consider different sets of worlds possible, because they have different information.
Epistemic logic handles nested knowledge and belief naturally. This is essential for multi-agent reasoning and for the BDI formalization in Section 7:
| Common notation | Standard notation | Meaning |
|---|---|---|
| □Bₐ | Bₐ(φ) | Agent a believes proposition B |
| ♢Dₐ | Desₐ(D) with ♢Dₐ as feasibility constraint | Agent a desires D. Note: ♢Dₐ (D is achievable in at least one accessible world) is a necessary condition for rational desire, not a definition of it. Desire is a separate attitude — see Section 7. |
| □Iₐ | Intₐ(I) | Agent a is committed to intention I. □Iₐ is the semantic rendering: Iₐ holds in every world a considers possible. Intₐ(I) is the full BDI operator, which interprets as □Iₐ plus the rationality constraint Intₐ(I) ⟹ Desₐ(I) ∧ ¬Bₐ(¬I). The □ gives the possible-worlds truth conditions; the consistency condition gives the constraints on what it means to rationally hold an intention. Intₐ(I) is a BDI-specific operator, not reducible to □ or ♢ by the □ alone. Defined formally in Section 7. |
| Bel_a(φ) | Bᵃφ | Agent a believes φ |
| K(φ) | Kᵃφ | Agent a knows φ |
Standard epistemic logic has a well-known and serious problem when applied to real agents: it implies agents are logically omniscient.
In standard possible-worlds semantics, two properties follow automatically:
The result: an agent that knows the axioms of arithmetic "knows" every provable theorem — including theorems that have never been proved and that mathematicians spend careers on. No real agent, human or artificial, works this way.
Aside — Gödel's incompleteness theorem and logical omniscience
Gödel's First Incompleteness Theorem (introduced in Section 1) gives a second, deeper reason why logical omniscience is unrealistic — beyond the obvious problem of infinite computation.
Standard epistemic logic assumes agents know all logical consequences of their beliefs. But if an agent's beliefs include the axioms of arithmetic, Gödel guarantees that some of those consequences are true but unprovable — no derivation of any finite length can reach them. So the assumption that agents know all consequences is not merely computationally unrealistic: it is logically impossible for any consistent system powerful enough to express arithmetic.
This means the logical omniscience problem has two distinct layers:
Layer 1 — computational: even for consequences that are provable, a real agent has finite time and memory and cannot derive all of them.
Layer 2 — logical (Gödel): for systems expressive enough to include arithmetic, some true consequences are not provable at all — no agent, no matter how powerful, can derive them within the system.
Konolige's bounded deduction model (below) addresses both layers at once: by restricting the agent to a finite rule set r applied to an explicit belief database Δ, the agent is neither expected to derive all provable consequences nor capable of reaching unprovable ones. The deductive closure close(Δ, r) is well-defined and reachable — though not necessarily finite, since some rule sets r can generate new propositions indefinitely.
For any realistic BDI agent: when formalizing a BDI proof using standard modal logic, you cannot simply assert □Bₐ and □Iₐ without acknowledging the logical omniscience problem. Acknowledge it explicitly and explain how you are restricting the agent's reasoning capacity — typically via Konolige's bounded deduction model.
Replace the possible-worlds definition of belief with an explicit deduction structure:
A deduction structure for agent a is a pair d = (Δ, r) where:
Δ is a finite set of propositions that the agent explicitly holds as beliefs — the belief database.
r is a finite set of inference rules that the agent can apply — possibly a strict subset of all valid inference rules.
This directly models resource-bounded reasoning. The agent only "knows" what it can actually compute from its explicit beliefs using its available rules. Consequences that require rules not in r — or derivation chains too long to compute — are simply not in the agent's belief set.
Applying Konolige's model to BDI reasoning:
When formalizing a BDI agent, state explicitly that it operates under a bounded deduction structure (Δ, r). Belief □Bₐ and intention □Iₐ hold only within the deductive closure close(Δ, r) — not over all logical consequences. Agent a does not automatically know every consequence of its beliefs; only those reachable by applying the rules in r to the database Δ. This restricts BDI reasoning to resource-bounded, computationally tractable agents and avoids the logical omniscience problem.
This section brings together everything from Sections 1–6 to formalize the Belief-Desire-Intention (BDI) framework in modal logic. It develops the rationality principle — the formal statement that a rational agent with consistent beliefs, desires, and intentions will act to fulfill those intentions in every accessible world — and works through the derivation step by step.
Notation note — accessibility relations in this tutorial
Three notations for accessibility relations appear across sections, each appropriate to its context:
All three mean the same underlying thing: the set of worlds the agent considers possible from the current world. The notation changes only to match the name of the agent in each context.
Let a be an agent. Let B, D, I be propositions representing the content of a's belief, desire, and intention respectively. Let w be the current world and Rₐ be a's accessibility relation — the set of worlds a considers possible from w.
Notational convention: the subscript a on Bₐ, Iₐ, Dₐ, Desₐ, Intₐ indicates that these are the propositional contents as held by agent a — distinguishing them from another agent's belief, intention, or desire in a multi-agent system. The propositions B, I, D themselves are plain propositions (goal states, facts about the world). The subscript a marks whose mental state we are describing. So □Bₐ means "the proposition Bₐ — B as held by agent a — is true in all worlds a considers possible," which is equivalent to saying "agent a believes B."
Why desire is not simply ♢Dₐ
A common notation error is to write ♢Dₐ for desire. But ♢Dₐ means "D is possible — D holds in at least one world a considers accessible." Possibility and desire are entirely different attitudes. An agent can consider it possible that it will rain without desiring rain at all. Conversely, an agent might desire something it considers impossible — though a rational agent would not.
Desire properly belongs to deontic logic — from the ancient Greek deon (δέον), meaning "that which is binding" or "duty" — the modal logic of goals, obligations, and permissions, where operators mean "it ought to be the case that" or "it is desired that," not "it is possible that." A full BDI formalization uses a separate desire operator Desₐ(D), not reducible to □ or ♢ without additional machinery.
The correct relationship is: ♢Dₐ is a necessary condition for rational desire — a rational agent Desₐ(D) only if ♢Dₐ also holds (the agent considers D achievable). But necessity is not sufficiency: ♢Dₐ does not imply Desₐ(D). We use Desₐ(D) for desire and note the feasibility constraint ♢Dₐ separately wherever it is needed.
This is the formal link between intentions and the other BDI states, due to Cohen and Levesque (1990):
This gives us a fundamental containment relationship between the sets of intentions and desires. Let I denote the set of all things agent a currently intends, and D the set of all things agent a currently desires. Then:
How does an agent form an intention? — Cohen & Levesque (1990)
The BDI consistency condition tells us what must be true once an intention is held. But how does an agent arrive at an intention in the first place? Intention formation is the upstream process that produces the premises □Bₐ, Desₐ(D), and □Iₐ that the BDI rationality derivation takes as given.
In the Cohen & Levesque formalization, intention formation is not modeled as a single operator — it is captured by the conditions under which Intₐ(I) becomes true. Roughly: the agent adopts Intₐ(I) when it has Desₐ(I), believes I is achievable (¬Bₐ(¬I)), and has selected I from competing desires via its planning process. Each of these maps directly onto a condition:
The BDI rationality derivation operates entirely downstream of this process. It takes the formed intention □Iₐ as a premise and reasons about what a rational agent does next — it does not model how the agent got there. Understanding intention formation clarifies why the BDI consistency condition has the shape it does: each term directly encodes one of the conditions above.
Act(a, I) is a proposition meaning "agent a performs an action directed at fulfilling intention I." It is true in world w if agent a executes, in w, an action whose goal is to bring about the state described by proposition I. Act(a, I) is the bridge between the agent's cognitive states and observable behavior.
The rationality principle connects all three BDI components to action. It is important to understand the distinct role each plays:
Provenance of the rationality principle
The formulation above is a pedagogical simplification inspired by Cohen & Levesque (1990) and Rao & Georgeff (1991), not a verbatim theorem from the literature. The canonical results in those papers use a richer temporal logic layer — operators like BEFORE, UNTIL, and HAPPENS — because intention and action play out over time: an agent commits to pursuing I until it is achieved or believed impossible, not just in a single snapshot of accessible worlds. That temporal machinery is beyond the scope of this tutorial. The principle as stated here captures the core idea faithfully at the level of standard modal logic. Do not cite it as a named theorem with a specific page reference.
What this derivation is — and is not
The rationality principle — (□Bₐ ∧ Desₐ(I) ∧ □Iₐ) ⟹ □(Act(a, I)) — cannot be derived from modal logic alone. It is a defining axiom of rational agency in the BDI framework: it states what we mean by calling an agent rational. It is not proven from more primitive truths — it is adopted as a definition.
What the derivation does accomplish is demonstrate that the conclusion follows from this axiom together with:
When presenting this formally, state: "The rationality principle is adopted as a defining axiom of rational agency in the BDI framework. The derivation demonstrates that the conclusion follows from this axiom together with the BDI consistency condition and the semantics of □."
This tutorial has covered the full formal machinery of modal and epistemic logic. You have the syntax of modal operators (Section 3), their semantics via possible worlds (Section 2), the axioms and what they mean for the accessibility graph (Section 4), the knowledge/belief distinction (Section 5), the bounded reasoning framework (Section 6), and the BDI formalization (Section 7). These tools are sufficient to formalize and reason about any BDI agent operating in a multi-agent environment.