直觉主义命题逻辑

直觉主义读法把“证明 $A\vee B$”理解为给出哪一边成立并提供相应证明，把“证明 $A\to B$”理解为把任意 $A$ 的证明转换成 $B$ 的证明。仅仅排除 $A$ 的反证失败，并没有产生 $A$ 的构造；因此从 $\neg \neg A$ 返回 $A$ 不是一般允许的操作。

这并非把经典真假改成固定的第三个真值。IPL 可以由证明、Heyting 代数、Kripke 信息增长等多种语义刻画；共同点是当前没有 $A$ 的证明与已经有 $\neg A$ 的证明不同。未决状态可以在获得更多信息后变为已证，而已证结论必须保持。

IPL 能证明 $A\to \mathrm{\neg }\mathrm{\neg }A$。先假设 $A$；为了证明 $\neg \neg A$，再假设 $\mathrm{\neg }A=A\to \mathrm{\perp }$，用 modus ponens 得到 $\perp$，随后依次解除两个假设。这是一条明确构造：给定 $A$ 的证明，就能把任何声称“$A$ 导致矛盾”的函数送到矛盾。

反向 $\mathrm{\neg }\mathrm{\neg }A\to A$ 没有同样的构造。取两个信息状态 $w_0\le w_1$，原子 $p$ 只在 $w_1$ 被证实。在 $w_0$，$p$ 尚未成立；$\mathrm{\neg }p$ 也不成立，因为未来 $w_1$ 会成立 $p$。于是 $w_0$ 不满足 $p\vee \mathrm{\neg }p$。这个直觉主义 Kripke 反模型公理库直觉主义 Kripke 语义Intuitionistic Kripke semantics · Kripke semantics for IPL在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。精确展示“尚未知道哪一边”，而不是给 $p$ 随意指定一个第三真值。

直觉主义并不禁止矛盾消去；从 $\perp$ 仍可推出任意命题。它拒绝的是不提供构造便把双重否定消掉。最小逻辑会进一步去掉 $\perp$ 消去，因此“非经典”也不自动等于“直觉主义”。

Heyting 代数公理库Heyting 代数Heyting algebra · Pseudo-Boolean algebra每个合取映射都有蕴涵右伴随的有界分配格，为直觉主义命题逻辑提供代数语义。把合取、析取与蕴涵解释为序结构中的运算，并给出 IPL 的代数可靠性与完备性。直觉主义 Kripke 语义公理库直觉主义 Kripke 语义Intuitionistic Kripke semantics · Kripke semantics for IPL在信息增长的预序世界上用持久赋值和未来量化解释直觉主义联结词的语义。则把世界解释成增长的信息状态，蕴涵量化全部未来扩张。两者都验证 IPL，却提供不同的证明工具与概念图像。

双重否定翻译公理库双重否定翻译Double-negation translation · Negative translation · Gödel–Gentzen negative translation通过系统插入双重否定，把经典命题证明嵌入直觉主义逻辑的负片段。把经典证明嵌入 IPL 的负片段：得到的是翻译后公式，而不是让原经典公式突然成为 IPL 定理。Gödel 翻译公理库Gödel 翻译Gödel translation · Gödel–McKinsey–Tarski translation给原子与蕴涵加上必然算子，把直觉主义命题逻辑忠实嵌入模态逻辑 S4。走另一条桥，把 IPL 公式送入模态逻辑 S4，用方框表达信息持久性。

经 Curry–Howard 对应，IPL 的证明对应简单类型 $\lambda$ 演算中的程序，$\to$ 对应函数类型、$\wedge$ 对应积类型、$\vee$ 对应和类型。该对应解释构造性，但不能把任意程序正确性自动归结为 IPL：递归、效应与依赖类型各需扩充语言和元理论。