直觉主义逻辑

直觉主义逻辑或构造性逻辑是最初由阿兰德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。直觉逻辑的公式的语法类似于命题逻辑或一阶逻辑。但是直觉逻辑的连结词不像经典逻辑那样是可互定义的，因此它们的选择是重要的。在直觉命题逻辑中通常使用 →, ∧, ∨, ⊥ 作为基本连结词，把 ¬ 作为 ¬A = (A → ⊥) 的简写处理。在直觉一阶逻辑中量词 ∃, ∀ 都是需要的。不同在于很多经典逻辑的重言式在直觉逻辑中不再是可证明的。例子不只包括排中律 P ∨ ¬P，还有皮尔士定律 ((P → Q) → P) → P，甚至还有双重否定除去。在经典逻辑中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直觉逻辑中，只有前者是定理: 双重否定可以介入但不能除去。对很多经典有效重言式不是直觉逻辑的定理的观察导致了弱化经典逻辑的证明论的想法。根岑发现简单限制他的系统LK（他的经典逻辑的相继式演算）就导致了关于直觉逻辑的一个可靠和完备的系统。他称之为系统LJ。推理规则是肯定前件，公理有:对于一阶逻辑系统还要加上普遍化规则，和如下公理:在经典命题逻辑中，有可能选取合取、析取或蕴涵中的一个作为原始的，并依据它和否定来定义另两个，比如在扬·武卡谢维奇的命题逻辑三公理中。甚至可以依据自足算子比如皮尔士箭头(NOR)或Sheffer竖线(NAND)定义它们四个。类似的，在经典一阶逻辑中，一个量词可以依据另一个量词和否定来定义。这是二值原理的推论，它使得这种连结词仅仅是布尔函数。二值原理在直觉逻辑中不成立，只有无矛盾律成立。作为结果没有连结词可以豁免，而上述公理都是必须的。多数经典恒等式只是直觉逻辑中在一个方向上的定理，尽管某些定理是两个方向的。它们如下:合取与析取:合取与蕴涵:析取与蕴涵:全称量词与存在量词:所以，例如 “a 或 b”是比“如果非 a 则 b”更强的陈述，而在经典逻辑中它们是可互换的。据 Alexander Kuznetsov 的证明，任一下述定义的连结词可以充当直觉逻辑的自足算子:语义要比经典逻辑更加复杂。其模型论可给出自海廷代数或等价的给出自克里普克语义。在经典逻辑中，我们经常讨论一个公式可能接受的真值。这种值通常被选择为布尔代数的成员。在布尔代数中的交和并算子等同于∧和∨逻辑连结词，所以形如A ∧ B的公式是在布尔代数中A的值和B的值的交。所以我们就有了一个有用的定理，一个公式是经典逻辑的有效的句子/断定，当且仅当它的值对于任何赋值都是1---就是说，对它的变量的任何指派都是真。对于直觉逻辑对应的法则也是真的，但是不再对每个公式指派（assign）来自布尔代数的值，而是使用来自海廷代数的值，布尔代数是它的特殊情况。公式在直觉逻辑中是有效的，当且仅当它对于在任何海廷代数上的任何赋值总是得到值1。可以证实为了识别有效的公式，考虑其元素是实平面R2的开集的一个单一的海廷代数就足够了。在这种代数中，∧和∨算子对应于集合的交集和并集，并且指派给公式A→B的值是 (AC ∪ B)o，它是B的值和A的值的补集的并集的内部。底元素是ø，顶元素是整个平面R2。¬A定义为A→ø，所以指派给它的值是ACo，这是A的值的补集的内部。通过这些指派，直觉上有效的公式正好就是被指派为整个平面的值的公式。例如，公式¬(A ∧ ¬A)是有效的，因为不管为公式A选择什么集合X作为值，¬(A ∧ ¬A)的值总是被证实为整个平面：一个拓扑学定理告诉我们XC°是XC的子集，所以交集为空，因此：所以这个公式的赋值是真，这个公式确实是有效的。但是排中律A∨¬A，可以被证实是“无效的”，通过设定A的值是{y : y > 0 }。那么¬A的值是{y : y ≤ 0 }的内部，它就是{y : y < 0 }，而公式的值是{y : y > 0 }和{y : y < 0 }的并集，这“不”是整个平面。上面描述的无限海廷代数对所有直觉上有效的公式给出了真赋值，而不管为公式中的变量指派了什么值。反过来说，对于每个无效的公式，都有来对变量的来自这个代数的一个值指派生成这个公式的一个假赋值。可以证实没有有限的海廷代数有这个性质。建立在他关于模态逻辑的语义的工作之上，索尔·阿伦·克里普克为直觉逻辑建立了另一套语义，叫做克里普克语义或关系语义。在古典逻辑的语义中，无论我们是否拥有对任何命题其中叙述情况的直接证据，命题公式都是从仅有两元素的集合 { ⊤ , ⊥ } {displaystyle {top ,bot }} （即为“true” 和“false”）而评估其真值。这被称之为“排中律”：因为它摒除了“为真” 或“为假” 之外的其它任何值存在的可能性。相较之下，直觉主义逻辑中的命题公式并不赋予明确的真值，只有在我们有直接证据时才被认为是 “真实的”，因此才具有证明。（我们也可说命题是由直接证据才据以成立，而并非命题公式本身的叙述就是“真”，它是由柯里-霍华德同构意义上的证据所支持的。）直觉主义逻辑中的操作因此保留了证据和可证明性方面的证据，而不单只执行真值的运算评估。直觉逻辑是开发数学建构主义方法的常用工具。建构主义逻辑的使用在数学家和哲学家中，一直是个争议话题（例如，参见 Brouwer-Hilbert 争议）。共同反对使用它们的意见是上面引用的缺乏古典逻辑的两个中心规则，即排中律和双重否定的消除规则。这被认为对大卫·希尔伯特所写的数学实践非常重要：“从数学家那里取走排中律不给他们使用，就像禁止望远镜给天文学家，或不允许拳击手使用他的拳头。禁止消除双否的存在陈述和排中律，等于完全放弃数学。”尽管直觉主义逻辑无法利用，排中律和双重否定的消除这两个对古典逻辑贡献极大的规则，而面临随之而来的严峻挑战，但直觉主义逻辑具有实际用途。其中一个原因是它所受的限制，反而因此产生了必须具备存在性的证据，使其也适用于其他形式的数学建构主义。非正式地，这意味着如果存在对象存在的建设性证据，则该构造性证据可用作生成该对象的示例算法，该原理即称为证明和算法之间的柯里-霍华德同构。直觉逻辑这种特性如此有价值的原因，是它使研究者能够使用广泛的计算机化工具，称为证明辅具。这些工具可以帮助用户验证（和生成）大规模的证据，这些证据的大小通常会排除发布和审查数学证据的常规人工检查。因此，使用证明辅具（例如 Agda 或 Coq）使现代数学家和逻辑学家能够开发和证明极其复杂的系统，远超出那些仅由手工创立和检查的系统。在这些工具出现之前，无法验证的著名范例是四色定理的证明。这个定理困扰了数学家一百多年，直到一个证据被开发出来，排除了大量可能的反例，但仍然留下可能性，需要一个计算机程序才能完成证明。这个证据在一段时间内引起争议，但最终使用 Coq 进行了验证。