A dual characterisation of simple and subdirectly-irreducible temporal Heyting algebras

TL;DR

This paper develops a duality theory for temporal Heyting algebras, characterizes simple and subdirectly-irreducible cases, and proves finite model properties for the associated temporal logic.

Contribution

It establishes an Esakia duality for temporal Heyting algebras and characterizes simple and subdirectly-irreducible cases using reachability notions.

Findings

Duality between temporal Heyting algebras and Esakia spaces

Finite case reachability notions are equivalent

Finite model property and relational completeness for the logic

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 {\guillemotleft} reachability {\guillemotright} 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.