# Bi-intuitionistic linear temporal logic

## Brett McLean

**Authors:** David Fernández-Duque, Brett McLean and Lukas Zenger

We investigate an intuitionistic propositional logic extended with both the co-implica-tion connective of Hilbert–Brouwer logic and with the modalities of linear temporal logic. We use a semantics based on intuitionistic Kripke frames equipped with an order-preserving function representing the temporal dynamics. By using the technical notion of a quasimodel, a type of nondeterministic encoding of a linear-time model, first introduced in [1], we establish the decidability of our bi-intuitionistic linear temporal logic and give a sound and complete Hilbert-style calculus for it. This work builds on that of [2], where the decidability of various bi-intuitionistic modal logics was established.

## Bibliography

- David Fern’andez-Duque,
*Non-deterministic semantics for dynamic topological logic*,,vol. 157 (2009), no. 2–3, pp. 110–121.*Annals of Pure and Applied Logic* - David Fern’andez-Duque, Brett McLean, and Lukas Zenger,
*A family of decidable bi-intuitionistic modal logics*,(Rhodes, Greece),(Pierre Marquis, Tran Cao Son, and Gabriele Kern-Isberner, editors),vol. 20,IJCAI Organization,2023,pp. 262–271.*proceedings of Principles of Knowledge Representation and Reasoning (KR)* - Cecylia Rauszer,
*Semi-boolean algebras and their applications to intuitionistic logic with dual operations*,, vol. 83 (1974) no. 3, pp. 219–249.*Fundamenta Mathematicae*