Temporal interpretation of intuitionistic quantifiers

MaRDI QIDQ6348118arXivFDO

Authors Guram Bezhanishvili, Luca Carai

Publication date 31 August 2020

Published in arXiv

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Temporal logic (03B44)

arXiv classification

math.LO

Abstract: We show that intuitionistic quantifiers admit the following temporal interpretation: $forallxA$ is true at a world $w$ iff $A$ is true at every object in the domain of every future world, and $existsxA$ 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 $sfS4.t$. The predicate logic $sf{Q}^{c}ircS4.t$ is obtained by weakening the axioms of the standard predicate extension $sfQS4.t$ of $sfS4.t$ along the lines Corsi weakened $sfQK$ to $sf{Q}^{c}ircK$. The G"odel translation embeds the predicate intuitionistic logic $sfIQC$ into $sfQS4$ fully and faithfully. We provide a temporal version of the G"odel translation and prove that it embeds $sfIQC$ into $sf{Q}^{c}ircS4.t$ fully and faithfully; that is, we show that a sentence is provable in $sfIQC$ iff its translation is provable in $sf{Q}^{c}ircS4.t$. Faithfulness is proved using syntactic methods, while we prove fullness utilizing the generalized Kripke semantics of Corsi.

This page was built for publication: Temporal interpretation of intuitionistic quantifiers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6348118)