The temporal Heyting calculus
David Quinn Alvarez

Abstract:
This thesis studies Esakia’s temporal Heyting calculus tHC, a temporal intuitionistic modal logic, by employing algebraic, topological, and frame-theoretic methods. First, we develop a general theory of temporal Heyting algebras, showing tHC to be sound and complete with respect to the variety and studying an important class of filters called ♦-filters as well as an important class of elements called ♦-compatible elements. Next, we develop a general theory of temporal Esakia spaces, studying an important class of subsets called archival subsets and using this notion to define two notions of « reachability » on our spaces : one order-topological and the other purely frame-theoretic. Next, we establish and develop an Esakia duality between the categories of temporal Heyting algebras and temporal Esakia spaces, including a full contravariant equivalence as well as a congruence/filter/closed-upset correspondence. Next, we use our duality theory to study the relational models of tHC, establishing relational soundness and completeness, developing a method of filtration on our models, and establishing the relational finite model property. Finally, we apply several of our duality and relational results to prove several facts about the variety of temporal Heyting algebras, including the algebraic finite model property. We conclude by proving the main results of the thesis : a lattice-theoretic and order-topological characterisation of both simple and subdirectly-irreducible temporal Heyting algebras (in both the general and finite case) as well as a final relational completeness result that combines finiteness and a type of « rootedness » defined in terms of the above-mentioned notion of « reachability ». We also include, in an appendix, a brief description of an algebraic symbolic model checker called thacheck that was authored for the variety of temporal Heyting algebras.