论文标题
直觉量词的时间解释
Temporal interpretation of intuitionistic quantifiers
论文作者
论文摘要
我们表明，直觉量化剂承认以下时间解释：$ \ forall x a $在世界上每个对象的每个对象中都是正确的，在每个未来世界的每个对象上都是正确的，而$ w $ a $在$ w $ iff $ a $上是正确的，在某些过去世界的某个域中，在某些对象中是正确的。为此，我们使用众所周知的时态命题逻辑$ \ sf s4.t $的谓词版本。谓词逻辑$ \ sf q^\ circ s4.t $是通过削弱标准谓词扩展的公理$ \ sf qs4.t $ \ sf sf s4.t $ of corsi沿Corsi削弱$ \ sf qk $ \ sf qk $ to $ \ sf q^q^\ sc Q^\ Circ k $。 Gödel翻译将谓词直觉逻辑$ \ sf iqc $嵌入到$ \ sf QS4 $中。我们提供了Gödel翻译的时间版本，并证明它将$ \ sf iqc $嵌入到$ \ sf q^\ circ s4.t $中；也就是说，我们证明句子在$ \ sf iqc $ iff中可证明其翻译可证明在$ \ sf q^\ circ s4.t $中。忠实是使用句法方法证明的，而我们利用Corsi的广义Kripke语义证明了充实。
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ödel translation embeds the predicate intuitionistic logic $\sf IQC$ into $\sf QS4$ fully and faithfully. We provide a temporal version of the Gödel 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.
