A decidable intuitionistic temporal logic

DOI10.4230/LIPICS.CSL.2017.14MaRDI QIDQ5111181zbMATH OpenOpenAlexFDO

Authors Joseph Boudou, Martín Diéguez, David Fernández-Duque

Publication date 26 May 2020

Full work available at URL https://arxiv.org/abs/1704.02847

zbMATH Keywords

intuitionistic logicproducts of modal logicstemporal logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Modal logic (including the logic of norms) (03B45)

Abstract: We introduce the logic $sfIT{L}^e$, an intuitionistic temporal logic based on structures $(W,preccurlyeq,S)$, where $preccurlyeq$ is used to interpret intuitionistic implication and $S$ is a $preccurlyeq$-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for $sfIT{L}^e$ are decidable. We prove this by showing that the logic enjoys the strong finite model property. In contrast, we also consider a `persistent' version of the logic, $sfIT{L}^p$, whose models are similar to Cartesian products. We prove that, unlike $sfIT{L}^e$, $sfIT{L}^p$ does not have the finite model property.

Recommendations

• Intuitionistic linear temporal logics
• A strongly complete axiomatization of intuitionistic temporal logic
• Complete intuitionistic temporal logics for topological dynamics
• Intuitionistic tense and modal logic
• Bisimulations for intuitionistic temporal logics

Cited in

(21)

• On the finite model property of weak intuitionistic tense logic
• Definability and decidability of binary predicates for time granularity
• Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
• scientific article; zbMATH DE number 1502114 (Why is no real title available?)
• The intuitionistic temporal logic of dynamical systems
• Decidable temporal and sequential relevant logics*
• Bisimulations for intuitionistic temporal logics
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• Complete intuitionistic temporal logics for topological dynamics
• Temporal interpretation of intuitionistic quantifiers
• A strongly complete axiomatization of intuitionistic temporal logic
• Intuitionistic linear temporal logics
• An intuitionistic axiomatization of `eventually'
• TEMPORAL INTERPRETATION OF MONADIC INTUITIONISTIC QUANTIFIERS
• Exploring the Jungle of Intuitionistic Temporal Logics
• Ill-founded proof systems for intuitionistic linear-time temporal logic
• Gödel-Dummett linear temporal logic
• Intuitionistic -calculus with the Lewis arrow
• On a generalization of Heyting algebras. I
• Decidability of logics based on an indeterministic metric tense logic
• On the interpretability of arithmetic in temporal logic

This page was built for publication: A decidable intuitionistic temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111181)