中间逻辑

中间逻辑是在直觉逻辑和经典逻辑之间的中介，这是在它们包含在直觉逻辑中不可证明的定理，而不导致完整的经典逻辑的意义上的。这种逻辑也叫做超直觉或次经典逻辑。

有連續統的勢个不同的中间逻辑，通常是向直觉逻辑增加一个或多个公理而获得的。 这种逻辑的例子有：

• 直觉逻辑 (IPC, Int, IL, H)
• 经典逻辑 (CPC, Cl, CL): IPC + P ∨ ¬P
• 弱排中律逻辑（KC, Jankov 逻辑，德·摩根定律逻辑）: IPC + ¬¬P ∨ ¬P
• 哥德尔-Dummett 逻辑 (LC): IPC + (P → Q) ∨ (Q → P)
• Kreisel-Putnam 逻辑：IPC +（¬P → (Q ∨ R)）→（(¬P → Q) ∨ (¬P → R))
• Medvedev 有限问题的逻辑
• 可实现性逻辑
• Scott 逻辑：IPC + ((¬¬P → P) → (P ∨ ¬P)) → (¬¬P ∨ ¬P)
• Smetanich 逻辑：IPC + (¬Q → P) →（（(P → Q) → P）→ P）研究中间逻辑的工具类似于直觉逻辑所使用的，比如Kripke语义。例如，Gödel-Dummett 逻辑有依据全序特征化的一个简单语义。

语义

给定一个 Heyting代数γ，在γ上有效的命题公式是中间逻辑。反过来说，给定一个中间逻辑可以构造出是 Heyting 代数的它的Lindenbaum代数。

一个直觉 Kripke框架 F 是偏序集合，而 Kripke 模型 M 是带有求值使得 $\{x\mid M,x\Vdash p\}$ 是 F 的上闭子集的 Kripke 框架。在 F 中有效的命题公式的集合是在中间逻辑中有效的。给定一个中间逻辑 Σ 有可能构造一个 Kripke 模型 M 使得 M 的逻辑是Σ（这种构造叫做“规范模型”）。带有这个性质的 Kripke 框架可能不存在，但是一般框架总是有。

与模态逻辑的关系

设 A 是命题公式。A 的“哥德尔-塔斯基变换”递归的定义如下：

• $T(p_n) = \Box p_n$
• $T(\neg A) = \Box \neg T(A)$
• $T(A \and B) = T(A) \and T(B)$
• $T(A \vee B) = T(A) \vee T(B)$
• $T(A \to B) = \Box (T(A) \to T(B))$

如果 Λ 是扩展 S4 的模态逻辑 则 ρΛ = {A | T(A) ∈ Λ} 是中间逻辑，而 Λ 叫做 ρΛ 的“模态伙伴”。特别是：

• IPC = ρS4
• KC = ρS4.2
• LC = ρS4.3
• CPC = ρS5

对于所有中间逻辑 Σ 都有很多模态逻辑 Λ 使得 Σ = ρΛ。

引用

• Toshio Umezawa. On logics intermediate between intuitionistic and classical predicate logic. Journal of Symbolic Logic, 24(2):141–153, June 1959.
• Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997.