用 Galois 连接刻画中间时态逻辑

我们提出了一种统一的方法，为每一个介于直觉主义逻辑和经典逻辑之间的逻辑 ${\sf L}$ 定义相应的中间最小时态逻辑 ${\sf LK_t}$。这是通过构建两个中间逻辑副本的融合并辅以 Galois 连接 ${\sf LGC}$ 来完成的，然后通过两个 Fischer Servi 公理互联它们的算子。由此产生的系统在此称为 ${\sf L2GC{+}FS}$。在直觉主义逻辑 ${\sf Int}$ 和经典逻辑 ${\sf Cl}$ 的情况下，注意到 ${\sf Int2GC{+}FS}$ 在句法上等价于 W. B. Ewald 提出的直觉主义最小时态逻辑 ${\sf IK_t}$，且 ${\sf Cl2GC{+}FS}$ 等于经典最小时态逻辑 ${\sf K_t}$。这证明了将 ${\sf L2GC{+}FS}$ 视为任何中间逻辑 ${\sf L}$ 的最小时态逻辑 ${\sf LK_t}$ 是合理的。我们将 H2GC+FS-代数定义为 E. Orlowska 和 I. Rewitzky 引入的 HK1-代数的扩张。对于每个中间逻辑 ${\sf L}$，我们证明了 ${\sf L2GC{+}FS}$ 的代数完备性及其相对于 ${\sf L}$ 的保守性。我们证明了 ${\sf Int2GC{+}FS}$ 关于 G. Fischer Servi 引入的 ${\sf IK}$-框架上定义的模型的关系完备性。我们还证明了一个表示定理，指出每个 H2GC+FS-代数都可以嵌入到其典范 ${\sf IK}$-框架的复代数中。