🚀 go-pugleaf

I hope this is the correct group in which to post an article on a
curiosity in epistemic logic.  It seems that there are a class of
sentences which, while true, may not be believed.  I'll give first
an example of an entirely reasonable statement, followed by a close
cousin which is unbelievable but true.

	let p = "it is raining"

	1.	Bel(Smith, p & ~Bel(Jones,p))

Smith believes that it is raining but that Jones doesn't believe it.

	2.	~Bel(Jones, p & ~Bel(Jones,p))

Note that in this case, p & ~Bel(Jones,p) may well be true, but that
Jones is incapable of believing it.
It's been a while since I've seen the derivation, but I recall that
the following is a theorem of epistemic logic:

	3.	(x)(p)~Bel(x, p & ~Bel(x,p))

provided that

	4.	Bel(x,p) > Bel(Bel(x,p))

is an axiom.

Good grief, my memory is getting rusty.  Is it S4 that is typically
used to model epistemic logics?

Anyway, can anyone out there add to this curious class of sentences?