# G"odel-Dummett linear temporal logic

arXiv: https://arxiv.org/abs/2306.15805 · HTML: https://mlsanity.com/paper/2306.15805/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 71 references that are in the map.
- First posted on arXiv 27 Jun 2023.

## Builds on (most cited first, 8 of 8)

- [On the complexity of Temporal Equilibrium Logic](https://mlsanity.com/paper/1503.00043/) (2015)
- [Intuitionistic Linear Temporal Logics](https://mlsanity.com/paper/1912.12893/) (2019)
- [A G"odel Calculus for Linear Temporal Logic](https://mlsanity.com/paper/2205.05182/) (2022)
- [G"odel Logic: from Natural Deduction to Parallel Computation](https://mlsanity.com/paper/1607.05120/) (2016)
- [Bisimulations for intuitionistic temporal logics](https://mlsanity.com/paper/1803.05078/) (2018)
- [On Transitive modal many-valued logics](https://mlsanity.com/paper/1904.01407/) (2019)
- [Some constructive variants of S4 with the finite model property](https://mlsanity.com/paper/2104.15053/) (2021)
- [Time and G"odel: Fuzzy temporal reasoning in PSPACE](https://mlsanity.com/paper/2205.00574/) (2022)

## Built on by (most cited first, 1 of 1)

- [Applications of Intuitionistic Temporal Logic to Temporal Answer Set Programming](https://mlsanity.com/paper/2603.14692/) (2026)

## Abstract (arXiv)

We investigate a version of linear temporal logic whose propositional fragment is G"odel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This G"odel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that G"odel temporal logic is PSPACE-complete. We also provide a deductive calculus for G"odel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus.