中間邏輯

中介邏輯是在直覺主義邏輯和經典邏輯之間的中介，這是在它們包含在直覺主義邏輯中不可證明的定理，而又不等於的經典邏輯的意義上說的。這種邏輯也叫做超直覺主義或次經典邏輯。

有連續統的勢個不同的中介邏輯，通常是向直覺主義邏輯增加一個或多個公理而獲得的。 這種邏輯的例子有：

• 直覺主義邏輯（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是帶有求值使得$\{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\land B)=T(A)\land 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

對於所有中介邏輯Σ都有很多模態邏輯Λ使得Σ = ρΛ。

參見

• 直覺主義
• 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.