G\"odel-Dummett linear temporal logic

TL;DR

This paper introduces G"odel-Dummett linear temporal logic, establishing its semantics, decidability, and proof calculus, and proves it to be PSPACE-complete with a sound and complete deductive system.

Contribution

It defines a novel G"odel-Dummett linear temporal logic with dual semantics, proves its decidability and PSPACE-completeness, and provides a sound and complete proof calculus.

Findings

Semantic equivalence of real-valued and bi-relational semantics

Decidability of the logic via finite quasimodels

PSPACE-completeness of the validity problem

Abstract

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.