Temporal interpretation of intuitionistic quantifiers

TL;DR

This paper provides a novel temporal interpretation of intuitionistic quantifiers using a predicate tense logic, embedding intuitionistic logic into a temporal modal framework with full faithfulness.

Contribution

It introduces a temporal interpretation of intuitionistic quantifiers and establishes a faithful and full embedding of intuitionistic logic into a predicate tense modal logic.

Findings

Temporal interpretation of $orall x A$ and $ eg orall x A$ in terms of future and past worlds.

Full and faithful embedding of intuitionistic logic into a predicate tense modal logic.

Use of generalized Kripke semantics to prove fullness.

Abstract

We show that intuitionistic quantifiers admit the following temporal interpretation: $\forall x A$ is true at a world $w$ iff $A$ is true at every object in the domain of every future world, and $\exists x A$ is true at $w$ iff $A$ is true at some object in the domain of some past world. For this purpose we work with a predicate version of the well-known tense propositional logic $\sf S4.t$. The predicate logic $\sf Q^\circ S4.t$ is obtained by weakening the axioms of the standard predicate extension $\sf QS4.t$ of $\sf S4.t$ along the lines Corsi weakened $\sf QK$ to $\sf Q^\circ K$. The G\"odel translation embeds the predicate intuitionistic logic $\sf IQC$ into $\sf QS4$ fully and faithfully. We provide a temporal version of the G\"odel translation and prove that it embeds $\sf IQC$ into $\sf Q^\circ S4.t$ fully and faithfully; that is, we show that a sentence is provable in $\sf IQC$ iff its translation is provable in $\sf Q^\circ S4.t$. Faithfulness is proved using syntactic methods, while we prove fullness utilizing the generalized Kripke semantics of Corsi.