Abstract
This work is a formalization of Stalnaker's epistemic logic with
countably many agents and its soundness and completeness theorems, as
well as the equivalence between the axiomatization of S4 available in
the Epistemic Logic theory and the topological one. It builds on the
Epistemic Logic theory.