I know that a topological pseudo-Boolean algebra is an algebra ⟨L, I, ¬, ∧, ∨, →⟩ such that ⟨L, ¬, ∧, ∨, →⟩ is an algebra and I an interior unary monotone operator on L, where the operator is defined as having many properties, e.g., Ia ≤ a for all a ∈ L, etc. An intuitionistic modal algebra is exactly this topological pseudo-Boolean algebra.
The Lindenbaum algebra of the topological Heyting algebra defined above is an intuitionistic modal algebra. The Lindenbaum algebra is an algebra containing the equivalence classes of sentences in the topological pseudo-Boolean algebra.
From this, we have that for any formula a ∈ L and the Lindenbaum algebra, a is true in the Lindenbaum algebra iff, when a is considered polynomial over the topological Heyting algebra, a = 1. Then, a formula a ∈ L is a theorem of IS4 (the canonical intuitionistic analogue of S4 modal logic) iff a = 1 in every topological Heyting algebra.
Beyond this, I'm struggling to find material which explains the model theory of a topological pseudo-Boolean algebra in depth, i.e., how models, truth, validity, soundness, completeness, etc. are defined.
Please can someone explain or introduce the algebraic formulation of these concepts for IS4, and moreover refer me to relevant material?