Temporal interpretation of monadic intuitionistic quantifiers

We show that monadic intuitionistic quantifiers admit the following temporal interpretation: "always in the future" (for for all) and "sometime in the past" (for there exists). It is well known that Prior's intuitionistic modal logic MIPC axiomatizes the monadic fragment of the intuitionistic predicate logic, and that MIPC is translated fully and faithfully into the monadic fragment MS4 of the predicate S4 via the Godel translation. To realize the temporal interpretation mentioned above, we introduce a new tense extension TS4 of S4 and provide a full and faithful translation of MIPC into TS4. We compare this new translation of MIPC with the Godel translation by showing that both TS4 and MS4 can be translated fully and faithfully into a tense extension of MS4, which we denote by MS4.t. This is done by utilizing the relational semantics for these logics. As a result, we arrive at the diagram of full and faithful translations shown in Figure 1 which is commutative up to logical equivalence. We prove the finite model property (fmp) for MS4.t using algebraic semantics, 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.