Math 2.0

Proposition

Axiom systems

Statement

Different modal logics can be derived from taking different subsets of these axioms, and these logics are normally named after the important axioms being employed. However, this is not always the case. KT45, the modal logic that results from the combining of K, T, 4, 5, and the Knowledge Generalization Rule, is primarily known as S5. This is why the properties of knowledge described above are often called the S5 Properties. However, it can be proven that modal axiom B is a theorem in S5 (viz. S5⊢𝐁S5 \vdash \mathbf {B}), which says that what an agent does not know that they do not know is true: ¬Ki¬Kiφ  ⟹  φ\neg K_i \neg K_i \varphi \implies \varphi. The modal axiom B is true on any symmetric frame, but is very counterintuitive in epistemic logic: How can the ignorance on one's own ignorance imply truth? It is therefore debatable whether S4 describes epistemic logic better, rather than S5.

Epistemic logic also deals with belief, not just knowledge. The basic modal operator is usually written B instead of K. In this case, though, the knowledge axiom no longer seems right—agents only sometimes believe the truth—so it is usually replaced with the Consistency Axiom, traditionally called D:

¬Bi⊥\neg B_i \bot

which states that the agent does not believe a contradiction, or that which is false. When D replaces T in S5, the resulting system is known as KD45. This results in different properties for 𝒦i\mathcal{K}_i as well. For example, in a system where an agent "believes" something to be true, but it is not actually true, the accessibility relation would be non-reflexive. The logic of belief is called doxastic logic.

Further reading

  1. Wikipedia, page 3827197, revision 1374360744, Epistemic modal logic, section The properties of knowledge > Axiom systems. adopted
About this page
TagP17XCCSQJM
URIm2://P17XCCSQJM
Kindstatement, proposition
WritingW0 stub
StatusThis copy of the site has no build data. Run m2 status P17XCCSQJM.
Changed4 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • edge uses out: each definition that the statement needs (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.