Paper detail

Temporal interpretation of intuitionistic quantifiers: Monadic case

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ö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ö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.