直觉主义量词的时间解释

我们证明直觉主义量词容许如下时间解释：$\forall x A$ 在世界 $w$ 为真当且仅当 $A$ 在每个未来世界的论域中的每个对象上为真，$\exists x A$ 在 $w$ 为真当且仅当 $A$ 在某个过去世界的论域中的某个对象上为真。为此我们使用著名的时态命题逻辑 $\sf S4.t$ 的谓词版本。谓词逻辑 $\sf Q^\circ S4.t$ 是通过沿 Corsi 将 $\sf QK$ 弱化至 $\sf Q^\circ K$ 的思路弱化 $\sf S4.t$ 的标准谓词扩张 $\sf QS4.t$ 的公理而得到的。Gödel 翻译将谓词直觉主义逻辑 $\sf IQC$ 完全且忠实地嵌入 $\sf QS4$。我们提供 Gödel 翻译的时间版本并证明它将 $\sf IQC$ 完全且忠实地嵌入 $\sf Q^\circ S4.t$；即我们证明一个句子在 $\sf IQC$ 中可证当且仅当其翻译在 $\sf Q^\circ S4.t$ 中可证。忠实性用语法方法证明，而完备性我们利用 Corsi 的广义 Kripke 语义证明。