A decidable intuitionistic temporal logic

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

Abstract: We introduce the logic

s f I T L^{e}

, an intuitionistic temporal logic based on structures

(W, p r e c c u r l y e q, S)

, where

p r e c c u r l y e q

is used to interpret intuitionistic implication and

S

is a

p r e c c u r l y e q

-monotone function used to interpret temporal modalities. Our main result is that the satisfiability and validity problems for

s f I T 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,

s f I T L^{p}

, whose models are similar to Cartesian products. We prove that, unlike

s f I T L^{e}

,

s f I T L^{p}

does not have the finite model property.

Recommendations

Cited in

(19)

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)