直觉主义逻辑

维基百科，自由的百科全书

直觉逻辑或构造性逻辑，是在数学直觉主义和其他形式的数学结构主义中使用的逻辑。

粗略的说，"直觉主义"把数学和逻辑保持为"构造性"的精神活动。就是说，它们不是解析性活动，在其中披露和应用存在的深入性质。转而，逻辑和数学是应用内部一致的方法，去认识更加复杂的精神构造(实际上是一种游戏)。在更严格的意义上，直觉逻辑可以作为非常具体和形式化的一种数理逻辑来研究。尽管对这样的一种形式化的演算是否实际上捕获了直觉主义的哲学特征是有争议的，在实用的观点上它是非常有用的工具。

下面给出这个术语的两重概念。

[编辑] 作为逻辑推理典范的直觉逻辑

在直觉逻辑中，证明中的在认识论上不清晰的步骤是禁止。在经典逻辑中，公式 A 断言 A 是真。在直觉逻辑中这个公式只在可被"证明"的情况下才被当作是真。作为这种区别的例子，考虑经典逻辑所接受的排中律，直觉逻辑不接受这条定律，因为在允许这种公式的语言中，有可能从 P ∨ ¬P 得出结论，而不需要知道这个析取中哪个是真的。在效果上，在直觉逻辑中，P ∨ ¬P 说明至少 P 或 ¬P 中的一个可以被证明，这比说它们的析取是真要强壮。

背后的想法是精神构造的有效性依赖于它与它的上下文(知觉)的一致。出于这种看法，认识论上的不透明性，在效果上是欺骗。

直觉逻辑在它的逻辑演算中用证实性替代了真实性。逻辑演算跨越生成导出命题的变换保持证实性，而不是真实性。

直觉逻辑给予多个哲学派别哲学上的支持，其中最著名的是 Michael Dummett 的反實在論。

[编辑] 作为形式逻辑演算的直觉逻辑

从实用的观点，也有使用直觉逻辑的强烈动机。实际上，如果你找寻像逻辑编程的自动推理，那么你明显的不只是对存在性的陈述感兴趣。计算机程序被假定用来计算答案，而不是去陈述一个答案。所以，在应用中你通常找寻一个给定的存在性断言的证据。此外，你可能关心能证明 ∃x : P(x)，但是对于它顾及的任何具体 b 却不能证明 P(b) 的证明系统。

为了以数学上精确的方式形式化直觉逻辑，需要模型论(语义)和适当的证明论。直觉逻辑的公式的语法类似于命题逻辑或一阶逻辑。明显的区别是这些经典逻辑的很多重言式(tautology)在直觉逻辑中不再是可证明的。这种例子不只包括排中律 P ∨ ¬P，还有 Peirce 定律 ((P → Q) → P) → P。

经典重言式在直觉逻辑中无效的更加熟悉的例子与所谓的双重否定除去有关。在经典逻辑中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直觉逻辑中，只有第一个是定理: 双重否定可以介入，但不能除去。在直觉逻辑中否定的解释不同于它在经典逻辑中的对应物。在经典逻辑中，¬P 断言 P 是假；在直觉逻辑中，¬P 断言 P 的证明是不可能的。上面在这两个蕴涵之间的不对称现在变得很显著。如果 P 是可证明的，则证明没有 P 的证明当然是不可能的；第一个蕴涵成立。但是第二个蕴涵失败了: 因为没有对 P 的证明是不可能的证明，我们不能从这种缺乏得出结论有 P 的证明。双重否定除去的一个弱化版本是 ¬¬¬P → ¬P 是可以证明的。

对很多经典的有效重言式不是直觉逻辑的定理的观察导致弱化经典逻辑的证明理论的想法。比如 Gentzen 获得了相继式演算 LK的一个弱化版本，他称之为 LJ。这就得到了适合的证明理论。

直觉逻辑的语义比经典的确定性的情况更加复杂。Heyting代数或等价的Kripke语义给出了它的语义。

[编辑] Heyting 代数语义

在经典逻辑中，我们经常讨论一个公式可能接受的真值。这种值通常被选择为布尔代数的成员。在布尔代数中的交和并算子等同于 ∧ 和 ∨ 逻辑连结词，所以形如 A ∧ B 的公式是在布尔代数中 A 的值和 B 的值的交。所以我们就有了一个有用的定理，一个公式是经典逻辑的有效的句子/断定，当且仅当它的值对于任何求值都是 1---就是说，对它的变量的任何指派都是真。

对于直觉逻辑对应的法则也是真的，但是不再对每个公式指派(assign)来自布尔代数的值，而是使用来自Heyting代数的值，布尔代数是它的特殊情况。公式在直觉逻辑中是有效的，当且仅当它对于在任何 Heyting 代数上的任何求值总是得到值 1。

可以证实为了识别有效的公式，考虑其元素是实平面 R² 的开集(open set)的一个单一的 Heyting 代数就足够了。在这种代数中，∧ 和 ∨ 算子对应于集合的交和并，并且指派给公式 A→B 的值同于指派给公式 ¬(A ∧ ¬B)的值。指派给 ¬F 的值是 F^C°，这是 F 的值的补集的内部。表示 1(真)的值是全集 R²。通过这些指派，直觉上有效的公式正好就是被指派为值 1 的公式。