中间逻辑

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

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

• 直觉主义逻辑（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逻辑相对于线序的Kripke模型完全。

语义

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

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

与模态逻辑的关系

主条目：模态对应

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

• ${\displaystyle T(p_{n})=\Box p_{n}}$ 
• ${\displaystyle T(\neg A)=\Box \neg T(A)}$ 
• ${\displaystyle T(A\land B)=T(A)\land T(B)}$ 
• ${\displaystyle T(A\vee B)=T(A)\vee T(B)}$ 
• ${\displaystyle T(A\to B)=\Box (T(A)\to T(B))}$ 

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

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

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

参见

• 直觉主义
• BHK释义
• 直觉类型论
• 经典逻辑
• 线性逻辑
• 构造性证明
• Curry-Howard对应
• 可计算性逻辑
• 博弈语义

引用

• 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.