Doxastic logic is a type of logic concerned with reasoning about beliefs. The term doxastic derives from the ancient Greek δόξα, doxa, which means "belief". Typically, a doxastic logic uses to mean "It is believed that is the case", and the set denotes a set of beliefs. In doxastic logic, belief is treated as a modal operator.
There is complete parallelism between a person who believes propositions and a formal system that derives propositions. Using doxastic logic, one can express the epistemic counterpart of Gödel's incompleteness theorem of metalogic, as well as Löb's theorem, and other metalogical results in terms of belief.
Types of reasoners
To demonstrate the properties of sets of beliefs, Raymond Smullyan defines the following types of reasoners:
- Accurate reasoner: An accurate reasoner never believes any false proposition. (modal axiom T)
- A conceited reasoner with rationality of at least type 1 (see below) will necessarily lapse into inaccuracy.
- Consistent reasoner: A consistent reasoner never simultaneously believes a proposition and its negation. (modal axiom D)
- Normal reasoner: A normal reasoner is one who, while believing also believes they believe p (modal axiom 4).
- Peculiar reasoner: A peculiar reasoner believes proposition p while also believing they do not believe Although a peculiar reasoner may seem like a strange psychological phenomenon (see Moore's paradox), a peculiar reasoner is necessarily inaccurate but not necessarily inconsistent.
- Reflexive reasoner: A reflexive reasoner is one for whom every proposition has some proposition such that the reasoner believes .
- If a reflexive reasoner of type 4 [see below] believes , they will believe p. This is a parallelism of Löb's theorem for reasoners.
- Unstable reasoner: An unstable reasoner is one who believes that they believe some proposition, but in fact does not believe it. This is just as strange a psychological phenomenon as peculiarity; however, an unstable reasoner is not necessarily inconsistent.
- Stable reasoner: A stable reasoner is not unstable. That is, for every if they believe then they believe Note that stability is the converse of normality. We will say that a reasoner believes they are stable if for every proposition they believe (believing: "If I should ever believe that I believe then I really will believe ").
- Modest reasoner: A modest reasoner is one for whom every believed proposition , only if they believe . A modest reasoner never believes unless they believe . Any reflexive reasoner of type 4 is modest. (Löb's Theorem)
- Queer reasoner: A queer reasoner is of type G and believes they are inconsistent—but is wrong in this belief.
- Timid reasoner: A timid reasoner does not believe [is "afraid to" believe ] if they believe
Increasing levels of rationality
- Type 1 reasoner: A type 1 reasoner has a complete knowledge of propositional logic i.e., they sooner or later believe every tautology (any proposition provable by truth tables). Also, their set of beliefs (past, present and future) is logically closed under modus ponens. If they ever believe and then they will (sooner or later) believe .
- This rule can also be thought of as stating that belief distributes over implication, as it's logically equivalent to
- Type 1* reasoner: A type 1* reasoner believes all tautologies; their set of beliefs (past, present and future) is logically closed under modus ponens, and for any propositions and if they believe then they will believe that if they believe then they will believe . The type 1* reasoner has "a shade more" self awareness than a type 1 reasoner.
- Type 2 reasoner: A reasoner is of type 2 if they are of type 1, and if for every and they (correctly) believe: "If I should ever believe both and , then I will believe ." Being of type 1, they also believe the logically equivalent proposition: A type 2 reasoner knows their beliefs are closed under modus ponens.
- Type 4 reasoner: A reasoner is of type 4 if they are of type 3 and also believe they are normal.
Gödel incompleteness and doxastic undecidability
Let us say an accurate reasoner is faced with the task of assigning a truth value to a statement. There exists a statement which the reasoner must either remain forever undecided about or lose their accuracy. One solution is the statement:
- S: "I will never believe this statement."
If the reasoner ever believes the statement it becomes falsified by that fact, making an untrue belief and hence making the reasoner inaccurate in believing S.
Therefore, since the reasoner is accurate, they will never believe Hence the statement was true, because that is exactly what it claimed. It further follows that the reasoner will never have the false belief that is false. And so the reasoner must remain forever undecided as to whether the statement is true or false.
The equivalent theorem is that for any formal system F, there exists a mathematical statement which can be interpreted as "This statement is not provable in formal system F". If the system F is consistent, neither the statement nor its opposite will be provable in it.
Inaccuracy and peculiarity of conceited reasoners
A reasoner of type 1 is faced with the statement "I will never believe this sentence." The interesting thing now is that if the reasoner believes they are always accurate, then they will become inaccurate. Such a reasoner will reason: "The statement in question is that I won't believe the statement, so if it's false then I will believe the statement. Because I am accurate, believing the statement means it must be true. So if the statement is false then it must be true. It's tautological that if a statement being false implies the statement, then that statement is true. Therefore the statement is true."
At this point the reasoner believes the statement, which makes it false. Thus the reasoner is inaccurate in believing that the statement is true. If the reasoner hadn't assumed their own accuracy, they would never have lapsed into an inaccuracy. Formally:
- [definition of ]
- [elementary tautology]
- [because ]
- [reasoner believes all tautologies]
- [the reasoner is of type 1]
- [the reasoner is conceited]
- [modus ponens 5 and 6]
- [because ]
Additionally, the reasoner is peculiar because they believe that they don't believe the statement (symbolically, which follows from because ) even though they actually believe it.
For systems, we define reflexivity to mean that for any (in the language of the system) there is some such that is provable in the system. Löb's theorem (in a general form) is that for any reflexive system of type 4, if is provable in the system, so is 
Inconsistency of the belief in one's stability
If a consistent reflexive reasoner of type 4 believes that they are stable, then they will become unstable. Stated otherwise, if a stable reflexive reasoner of type 4 believes that they are stable, then they will become inconsistent. Why is this? Suppose that a stable reflexive reasoner of type 4 believes that they are stable. We will show that they will (sooner or later) believe every proposition (and hence be inconsistent). Take any proposition The reasoner believes hence by Löb's theorem they will believe (because they believe where is the proposition and so they will believe which is the proposition ). Being stable, they will then believe 
- Smullyan, Raymond M., (1986) Logicians who reason about themselves, Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, Monterey (CA), Morgan Kaufmann Publishers Inc., San Francisco (CA), pp. 341–352
- https://web.archive.org/web/20070930165226/http://cs.wwc.edu/KU/Logic/Book/book/node17.html Belief, Knowledge and Self-Awareness[dead link]
- https://web.archive.org/web/20070213054220/http://moonbase.wwc.edu/~aabyan/Logic/Modal.html Modal Logics[dead link]
- Smullyan, Raymond M., (1987) Forever Undecided, Alfred A. Knopf Inc.
- Rod Girle, Possible Worlds, McGill-Queen's University Press (2003) ISBN 0-7735-2668-4 ISBN 978-0773526686
- Lindström, St.; Rabinowicz, Wl. (1999). "DDL Unlimited. Dynamic Doxastic Logic for Introspective Agents". Erkenntnis. 51 (2–3): 353–385. doi:10.1023/A:1005577906029.
- Linski, L. (1968). "On Interpreting Doxastic Logic". Journal of Philosophy. 65 (17): 500–502. JSTOR 2024352.
- Segerberg, Kr. (1999). "Default Logic as Dynamic Doxastic Logic". Erkenntnis. 50 (2–3): 333–352. doi:10.1023/A:1005546526502.
- Wansing, H. (2000). "A Reduction of Doxastic Logic to Action Logic". Erkenntnis. 53 (1–2): 267–283. doi:10.1023/A:1005666218871.