nLab epistemic modal logic

Epistemic logic

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Modality

Epistemic logic

Idea

Epistemic logic is the branch of modal logic which is concerned with epistemology, hence with notions of knowledge and sometimes also notions of belief, although these may be treated separately by doxastic logic. In its applied form it has found considerable use in computer science and Artificial Intelligence.

The key modal operators for epistemic logic are forms of necessity and possibility corresponding to “It is known to be the case that” and “It may be the case that (so far as is known)”. As a form of modal logic, the semantics typically used is possible worlds semantics where the worlds correspond to maximally specific ways the world could have been. Philosophers disagree as to whether to distinguish the space of metaphysically possible worlds from the space of epistemically possible worlds (Kment 21).

Introduction

Epistemic modalities are captured in epistemic modal logic by interpreting “necessarily ϕ\phi” as saying “It is known that proposition ϕ\phi is true”. It is common also to indicate the epistemic agent, so that corresponding to agent xx we have “xx knows that proposition ϕ\phi is true”.

In the closely related ‘provability logic’, the basic modal operator interprets as “it is provable that ϕ\phi.

Notice that the notions of possibility and necessity have different senses in ordinary language. For example, if we say ‘PP is possible’, we may mean that PP is: epistemically possible, not ruled out by anything I know; physically possible, not ruled out by the laws of physics; logically possible, not ruled out by the laws of logic. Some suggest that there is a further type of possibility, metaphysical possibility intermediate between logical and physical possibility. Metaphysical possibility would allow that different laws of physics might apply.

Epistemic formulae

These are variants of the formulae of the basic modal language. The basic modal operators are, here, labelled K iK_i since they relate to ‘knowledge’ and indicate the epistemic agent, the knower, ii. These correspond to the \Box operators in the standard form, and are used in preference to the dual \Diamond forms since they are more immediately relevant to applications.

More formally, we have PP or PropProp, is a set of countably (finite or infinite) many atomic formulae. there is also a set AA, often called the set of ‘agents’ and taken to be A={1,,m}A = \{1,\ldots,m\}. The set of epistemic formulae (= basic mm-agent epistemic language) will be denoted K m(P)\mathcal{L}^m_K(P) is given by the rules

ϕ::=p¬ϕϕ 1ϕ 2K iϕforiA.\phi ::= p \mid \bot \mid \neg \phi \mid \phi_1 \wedge \phi_2 \mid K_i\phi for i\in A.

We read K iϕK_i \phi as ‘’agent ii knows that ϕ\phi’’.

The converse or dual operators, denoted M iM_i (so that M iϕ=¬K i¬ϕM_i \phi = \neg K_i\neg \phi) reads as ‘’agent ii considers ϕ\phi is possible’’.

Note

The ‘agent’ terminology is extremely useful, but in pure modal logic texts is not used so much. It does provide an ‘intuition’ and an interpretation however.

Axioms for epistemic logic

The question then arises as to which axioms of modal logic are appropriate to the epistemic case. Answers will depend on what interpretation is given to `know' in specifying how the operator $K$ behaves. E.g., there is a difference between the knowledge of a realistic, cognitively-limited agent and that of some idealized agent with boundless resources.

It is generally admitted that axiom (T) should hold, here

T:Kϕϕ, \mathbf{T}: K \phi \to \phi,

which states that if ϕ\phi is known then ϕ\phi is true. Truth is generally taken to be a precondition of knowledge.

A much more contentious issue in the field is whether to admit an epistemic version of axiom (4). This corresponds to

4:KϕKKϕ, \mathbf{4}: K \phi \to K K \phi,

which states that when ϕ\phi is known to be true then it is also known that it is known.

It is even possible to challenge the admission of two of the most fundamental modal axioms, axioms (N) and (K). These correspond to

N,:,If,P,is a theorem, then so is,KP \mathbf{N} \phantom{,}\colon\phantom{,} \text{If}\phantom{,}P\phantom{,}\text{is a theorem, then so is}\phantom{,}K P

and

K:K(PQ)(KPKQ). \mathbf{K}: K(P \to Q) \to (K P \to K Q).

An understanding of N that it states that all theorems are known is evidently problematic. Similarly for K, it is not clear that we know the deductive consequences of the collection of propositions that we know, such as the application of modus ponens to every instance of known PQP \to Q and PP.

On the other hand, we might consider epistemic logic to represent the reasoning of an ideal, logically omniscient, agent, and so admit N and K.

Models for epistemic logics

The geometric or combinatorial semantics of epistemic models follows the same techniques of Kripke frames as at geometric models for modal logics, whilst the algebraic models are BAOs that is Boolean algebras with operators. As usual the Kripke frames semantics is an example of coalgebraic semantics?.

References

A fairly recent book on epistemic logics and their applications (which was used for some of the material above):

  • J.- J. Ch. Meyer and W. Van der Hoek, Epistemic logic for AI and Computer Science, Cambridge Tracts in Theoretical Computer Science, vol. 41, 1995,

General books on modal logic with discussion of epistemic logic:

  • Patrick Blackburn, M. de Rijke and Yde Venema, Modal Logic, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001.

  • Marcus Kracht, Tools and Techniques in Modal Logic, Studies in Logic and the Foundation of Mathematics, 142, Elsevier, 1999,

  • Johan van Benthem, Dynamic logic for belief revision (pdf)

  • Boris Kment, Varieties of Modality, SEP

See also:

Last revised on March 17, 2023 at 17:00:36. See the history of this page for a list of all contributions to it.