Doxatic logic & types of reasoners

https://en.wikipedia.org/wiki/Doxastic_logic 
Something i read long time back when i read Smullyan's books, but making a note because i love it. His types of reasoners is beautiful :)

Types of reasoners[edit]

To demonstrate the properties of sets of beliefs, Raymond Smullyan defines the following types of reasoners:

• Accurate reasoner:^[1][2][3][4] An accurate reasoner never believes any false proposition. (modal axiom T)

${\displaystyle \forall p:{\mathcal {B}}p\to p}$

• Inaccurate reasoner:^[1][2][3][4] An inaccurate reasoner believes at least one false proposition.

${\displaystyle \exists p:\neg p\wedge {\mathcal {B}}p}$

• Conceited reasoner:^[1][4] A conceited reasoner believes his or her beliefs are never inaccurate.

${\displaystyle {\mathcal {B}}[\neg \exists p(\neg p\wedge {\mathcal {B}}p)]\quad {\text{or}}\quad {\mathcal {B}}[\forall p({\mathcal {B}}p\to p)]}$

A conceited reasoner with rationality of at least type 1 (see below) will necessarily lapse into inaccuracy.

• Consistent reasoner:^[1][2][3][4] A consistent reasoner never simultaneously believes a proposition and its negation. (modal axiom D)

${\displaystyle \neg \exists p:{\mathcal {B}}p\wedge {\mathcal {B}}\neg p\quad {\text{or}}\quad \forall p:{\mathcal {B}}p\to \neg {\mathcal {B}}\neg p}$

• Normal reasoner:^[1][2][3][4] A normal reasoner is one who, while believing ${\displaystyle p,}$ also believes he or she believes p (modal axiom 4).

${\displaystyle \forall p:{\mathcal {B}}p\to {\mathcal {BB}}p}$

• Peculiar reasoner:^[1][4] A peculiar reasoner believes proposition p while also believing he or she does not believe ${\displaystyle p.}$ 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.

${\displaystyle \exists p:{\mathcal {B}}p\wedge {\mathcal {B\neg B}}p}$

• Regular reasoner:^[1][2][3][4] A regular reasoner is one who, while believing ${\displaystyle p\to q}$, also believes ${\displaystyle {\mathcal {B}}p\to {\mathcal {B}}q}$.

${\displaystyle \forall p\forall q:{\mathcal {B}}(p\to q)\to {\mathcal {B}}({\mathcal {B}}p\to {\mathcal {B}}q)}$

• Reflexive reasoner:^[1][4] A reflexive reasoner is one for whom every proposition ${\displaystyle p}$ has some proposition ${\displaystyle q}$ such that the reasoner believes ${\displaystyle q\equiv ({\mathcal {B}}q\to p)}$.

${\displaystyle \forall p:\exists q{\mathcal {B}}(q\equiv ({\mathcal {B}}q\to p))}$

If a reflexive reasoner of type 4 [see below] believes ${\displaystyle {\mathcal {B}}p\to p}$, he or she will believe p. This is a parallelism of Löb's theorem for reasoners.

• Unstable reasoner:^[1][4] An unstable reasoner is one who believes that he or she believes 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.

${\displaystyle \exists p:{\mathcal {B}}{\mathcal {B}}p\wedge \neg {\mathcal {B}}p}$

• Stable reasoner:^[1][4] A stable reasoner is not unstable. That is, for every ${\displaystyle p,}$ if he or she believes ${\displaystyle {\mathcal {B}}p}$ then he or she believes ${\displaystyle p.}$ Note that stability is the converse of normality. We will say that a reasoner believes he or she is stable if for every proposition ${\displaystyle p,}$ he or she believes ${\displaystyle {\mathcal {B}}{\mathcal {B}}p\to {\mathcal {B}}p}$ (believing: "If I should ever believe that I believe ${\displaystyle p,}$ then I really will believe ${\displaystyle p}$").

${\displaystyle \forall p:{\mathcal {BB}}p\to {\mathcal {B}}p}$

• Modest reasoner:^[1][4] A modest reasoner is one for whom every believed proposition ${\displaystyle p}$, ${\displaystyle {\mathcal {B}}p\to p}$ only if he or she believes ${\displaystyle p}$. A modest reasoner never believes ${\displaystyle {\mathcal {B}}p\to p}$ unless he or she believes ${\displaystyle p}$. Any reflexive reasoner of type 4 is modest. (Löb's Theorem)

${\displaystyle \forall p:{\mathcal {B}}({\mathcal {B}}p\to p)\to {\mathcal {B}}p}$

• Queer reasoner:^[4] A queer reasoner is of type G and believes he or she is inconsistent—but is wrong in this belief.
• Timid reasoner:^[4] A timid reasoner does not believe ${\displaystyle p}$ [is "afraid to" believe ${\displaystyle p}$] if he or she believes ${\displaystyle {\mathcal {B}}p\to {\mathcal {B}}\bot }$

Curry Howard Correspondence

Came across this which is a link between computer programs and logic, in the sense that using computer programs to "prove" things is legit. My interpretation of this is that it shows that constructs we use in computers languages can solve the same problems we solve using logic --

https://www.quora.com/Why-is-the-Curry-Howard-isomorphism-interesting

Not really a big deal, but something to make a note of, for future reference.

python multiprocessing module

https://www.usenix.org/system/files/login/articles/login1210_beazley.pdf