Characterizing intermediate tense logics in terms of Galois connections
Characterizing intermediate tense logics in terms of Galois connections
复制标题
用伽罗瓦连接表征中间时态逻辑
DOI：
10.1093/jigpal/jzu024
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. Kondo
中科院分区：
文献类型：
--
作者：
W. Dzik;Jouni Järvinen;M. Kondo
我们提出了一种统一的方法来定义直觉逻辑和经典逻辑之间的每个逻辑${\sf L}$，相应的中间最小时态逻辑${\sf LK_t}$。这是通过使用伽罗瓦连接 ${\sf LGC}$ 构建中间逻辑的两个副本的融合，然后通过两个 Fischer Servi 公理互连它们的运算符来完成的。由此产生的系统在此称为${\sf L2GC{+}FS}$。在直觉逻辑 ${\sf Int}$ 和经典逻辑 ${\sf Cl}$ 的情况下，值得注意的是 ${\sf Int2GC{+}FS}$ 在语法上等同于 W. B. Ewald 和 ${\sf 的直觉最小时态逻辑 ${\sf IK_t}$ Cl2GC{+}FS}$ 等于经典最小时态逻辑 ${\sf K_t}$。这证明将 ${\sf L2GC{+}FS}$ 视为任何中间逻辑 ${\sf L}$ 的最小 ${\sf L}$ 时态逻辑 ${\sf LK_t}$ 是合理的。我们将 H2GC+FS 代数定义为 HK1 代数的扩展，由 E. Orlowska 和 I. Rewitzky 提出。对于每个中间逻辑 ${\sf L}$，我们展示了 ${\sf L2GC{+}FS}$ 的代数完备性及其相对于 ${\sf L}$ 的保守性。我们证明了 ${\sf Int2GC{+}FS}$ 相对于 G. Fischer Servi 引入的 ${\sf IK}$ 框架上定义的模型的关系完整性。我们还证明了一个表示定理，指出每个 H2GC+FS 代数都可以嵌入到其规范 ${\sf IK}$ 框架的复代数中。
We propose a uniform way of defining for every logic ${\sf L}$ intermediate between intuitionistic and classical logics, the corresponding intermediate minimal tense logic ${\sf LK_t}$. This is done by building the fusion of two copies of intermediate logic with a Galois connection ${\sf LGC}$, and then interlinking their operators by two Fischer Servi axioms. The resulting system is called here ${\sf L2GC{+}FS}$. In the cases of intuitionistic logic ${\sf Int}$ and classical logic ${\sf Cl}$, it is noted that ${\sf Int2GC{+}FS}$ is syntactically equivalent to intuitionistic minimal tense logic ${\sf IK_t}$ by W. B. Ewald and ${\sf Cl2GC{+}FS}$ equals classical minimal tense logic ${\sf K_t}$. This justifies to consider ${\sf L2GC{+}FS}$ as minimal ${\sf L}$-tense logic ${\sf LK_t}$ for any intermediate logic ${\sf L}$. We define H2GC+FS-algebras as expansions of HK1-algebras, introduced by E. Orlowska and I. Rewitzky. For each intermediate logic ${\sf L}$, we show algebraic completeness of ${\sf L2GC{+}FS}$ and its conservativeness over ${\sf L}$. We prove relational completeness of ${\sf Int2GC{+}FS}$ with respect to the models defined on ${\sf IK}$-frames introduced by G. Fischer Servi. We also prove a representation theorem stating that every H2GC+FS-algebra can be embedded into the complex algebra of its canonical ${\sf IK}$-frame.