Proof and Model Theory of Intuitionistic Temporal Logic
University of Bern - University of Ghent
SNSF-FWO Lead Agency Project 200021L_196176/G0E2121N


Our Project

Intuitionistic logic enjoys a myriad of interpretations based on computation, information or topology, making it a natural framework to reason about dynamic processes in which these phenomena play a crucial role. However, there is a large gap to be filled regarding our understanding of the computational behaviour of intuitionistic temporal logics. The aim of this project is to cement our understanding of intuitionistic temporal logics by developing their model theory based on dynamic topological systems, and their proof theory based on prominent paradigms such as Gentzen-style calculi as well as cyclic proofs.

Bern Team
  • Supervisor:
    Thomas Studer [webpage]

  • PhD Student:
    Lukas Zenger [webpage]
Ghent Team
  • Supervisors:
    David Fernández-Duque [webpage]
    Andreas Weiermann [webpage]

  • Postdoctoral Researcher:
    Brett McLean [webpage]
Publications
  • Joseph Boudou, Martín Diéguez and David Fernández-Duque. Complete Intuitionistic Temporal Logics in Topological Dynamics. Journal of Symbolic Logic, DOI: https://doi.org/10.1017/jsl.2022.8, 2022. [Journal] [ArXiv]
  • Joseph Boudou, Martín Diéguez, and Philip Kremer. Exploring the Jungle of Intuitionistic Temporal Logics. Theory and Practice of Logic Programming, 21(4): 459-492 (2021) [Journal] [ArXiv]
  • Philippe Balbiani, Martín Diéguez, and David Fernández-Duque. Some constructive variants of S4 with the finite model property. LICS 2021: 1-13. [Proceedings] [ArXiv]