A dual characterisation of simple and subdirectly-irreducible temporal Heyting algebras
David Quinn Alvarez
TL;DR
The paper develops Esakia duality between temporal Heyting algebras $\mathbf{tHA}$ and temporal Esakia spaces $\mathbf{tES}$, redefining dualities with $R^{\triangleleft}$ and $\blacklozenge$ to obtain a contravariant equivalence and a congruence/filter/closed-upset correspondence. It introduces two reachability notions—topological on $\mathbf{tES}$ and frame-based on $\mathbf{tTran}_{\textsf{fin}}$—and proves their equivalence in the finite setting, enabling lattice-theoretic and dual characterisations of simple and subdirectly-irreducible algebras. Using the duality, the authors establish relational and algebraic finite model properties for the temporal Heyting calculus $\mathbf{tHC}$, and derive a relational completeness result that relies on finite, frame-structured models dual to subdirect-irreducibility. The results yield a robust, finite, well-understood frame theory for a sub-classical temporal logic and provide a dual toolkit linking algebraic and relational semantics for $\mathbf{tHC}$.
Abstract
We establish an Esakia duality for the categories of temporal Heyting algebras and temporal Esakia spaces. This includes a proof of contravariant equivalence and a congruence/filter/closed-upset correspondence. We then study two notions of « reachability » on the relevant spaces/frames and show their equivalence in the finite case. We use these notions of reachability to give both lattice-theoretic and dual order-topological characterisations of simple and subdirectly-irreducible temporal Heyting algebras. Finally, we apply our duality results to prove the relational and algebraic finite model property for the temporal Heyting calculus. This, in conjunction with the proven characterisations, allows us to prove a relational completeness result that combines finiteness and the frame property dual to subdirect-irreducibility, giving us a class of finite, well-understood frames for the logic.