Temporal interpretation of intuitionistic quantifiers: Monadic case

TL;DR

This paper explores a new temporal interpretation of monadic intuitionistic quantifiers by introducing a tense extension of S4, providing full and faithful translations and establishing the finite model property for the extended logic.

Contribution

It introduces the tense logic TS4 and demonstrates its full and faithful translation of monadic intuitionistic logic, extending the G"odel translation and analyzing algebraic and relational semantics.

Findings

TS4 provides a temporal interpretation of monadic intuitionistic quantifiers.

Full and faithful translations between MIPC, TS4, and MS4.t are established.

Finite model property is proven for MS4.t.

Abstract

In a recent paper we showed that intuitionistic quantifiers admit the following temporal interpretation: "always in the future" (for $\forall$) and "sometime in the past" (for $\exists$). In this paper we study this interpretation for the monadic fragment $\sf MIPC$ of the intuitionistic predicate logic. It is well known that $\sf MIPC$ is translated fully and faithfully into the monadic fragment $\sf MS4$ of the predicate $\sf S4$ (G\"{o}del translation). We introduce a new tense extension of $\sf S4$, denoted by $\sf TS4$, and provide an alternative full and faithful translation of $\sf MIPC$ into $\sf TS4$, which yields the temporal interpretation of monadic intuitionistic quantifiers mentioned above. We compare this new translation with the G\"{o}del translation by showing that both $\sf MS4$ and $\sf TS4$ can be translated fully and faithfully into a tense extension of $\sf MS4$, which we denote by $\sf MS4.t$. This is done by utilizing the algebraic and relational semantics for the new logics introduced. As a byproduct, we prove the finite model property (fmp) for $\sf MS4.t$ and show that the fmp for the other logics involved can be derived as a consequence of the fullness and faithfulness of the translations considered.