  The foundations of formal models for epistemic and doxastic logics often rely
on certain logical aspects of modal logics such as S4 and S4.2 and their
semantics; however, the corresponding mathematical results are often stated in
papers or books without including a detailed proof, or a reference to it, that
allows the reader to convince themselves about them. We reinforce the
foundations of the epistemic logic S4.2 for countably many agents by
formalizing its soundness and completeness results for the class of all
weakly-directed pre-orders in the proof assistant Isabelle/HOL. This logic
corresponds to the knowledge fragment, i.e., the logic for formulas that may
only include knowledge modalities in Stalnaker's system for knowledge and
belief. Additionally, we formalize the equivalence between two axiomatizations
for S4, which are used depending on the type of semantics given to the modal
operators, as one is commonly used for the relational semantics, and the other
one arises naturally from the topological semantics.
