Title：A Sound and Complete Axiomatization for Intuitionistic Linear Temporal Logic

Speaker：Lukas Zenger (University of Bern)

Time: 2024/11/12 15:10-18:00

Location: Room 206, Building of Geometry (地学楼), Peking University

Abstract：

Intuitionistic linear temporal logic iLTL extends intuitionistic propositional logic with the temporal modalities 'next', 'eventually' and 'henceforth'. Formulas are evaluated over expanding models, i.e. intuitionistic Kripke models equipped with an order-preserving function representing the temporal dynamics. The mathematical theory of iLTL has been studied extensively in recent years, resulting, amongst others, in a decidability proof for iLTL over expanding models. However, providing a sound and complete axiomatization has remained an open problem.

In this talk I will first summarize the state of the field, including some of the main results about the proof theory and model theory of (fragments of) iLTL. I will then propose an extension of iLTL with the co-implication connective of Heyting-Brouwer logic called bi-intuitionistic linear temporal logic biLTL. By using the technical notion of a quasimodel, I will show that this extension is still decidable for the class of expanding models. Moreover, I present a sound and complete Hilbert-style calculus for biLTL, the first for any logic extending iLTL. As an unexpected corollary, I will show that no notion of co-implication is definable in a topological setting validating bi-intuitionistic logic.

This is joint work with David Fernández-Duque (University of Barcelona) and Brett McLean (Ghent University).