直觉主义逻辑与反证法

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

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

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

目录 1 作为逻辑推理典范的直觉逻辑 2 作为形式逻辑演算的直觉逻辑 3 Heyting 代数语义 4 Kripke 语义 5 参见 6 外部链接
//

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

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

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

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

[编辑] 作为形式逻辑演算的直觉逻辑
从实用的观点，也有使用直觉逻辑的强烈动机。实际上，如果你找寻像逻辑编程的自动推理，那么你明显的不只是对存在性的陈述感兴趣。计算机程序被假定用来计算答案，而不是去陈述一个答案。所以，在应用中你通常找寻一个给定的存在性断言的证据。此外，你可能关心能