直觉主义逻辑是一种将构造性推理形式化的逻辑学系统：确立一个命题需要提供适当的证据，而不能仅仅排除它为假的可能。它为构造性数学提供了逻辑基础，与经典逻辑的主要区别在于不接受不受限制的排中律或双重否定消去。其标准形式包括命题逻辑和一阶逻辑。它们分别是相应经典逻辑的真子系统：每个在直觉主义逻辑中可证明的公式，在经典逻辑中也可证明，反之则不成立。(plato.stanford.edu)
历史发展
这一领域源于 L. E. J. 布劳威尔在二十世纪初提出的直觉主义。直觉主义将数学对象视为构造的产物，而不是独立存在的抽象实体。布劳威尔质疑不受限制地应用经典逻辑原则，尤其是将这些原则用于无限集合。1930 年，阿伦德·海廷发表了直觉主义命题逻辑、谓词逻辑和算术的形式系统，使这些原则得以接受系统的数学研究。(math.ucla.edu)
海廷对证明的阐释，以及安德烈·柯尔莫哥洛夫将命题解释为问题的观点，共同推动了现代构造性解释的发展。1932 年，柯尔莫哥洛夫用问题及其解来描述逻辑运算。由此形成的证明解释后来被称为布劳威尔—海廷—柯尔莫哥洛夫解释，简称 BHK 解释。研究这一形式逻辑，并不要求接受布劳威尔更广泛的哲学立场。(plato.stanford.edu)
联结词的构造性含义
BHK 解释通过说明什么算作数学证明来解释逻辑运算：
- (A\land B) 的证明同时提供 (A) 的证明和 (B) 的证明。
- (A\lor B) 的证明提供某个确定分支的证明，并指出所确立的是哪一个分支。
- (A\to B) 的证明提供一种构造，能将 (A) 的任意证明转化为 (B) 的证明。
- (\exists x,P(x)) 的证明提供一个见证对象，并证明该对象满足 (P)。
- (\forall x,P(x)) 的证明提供一种统一的构造，能为论域中的任意对象给出 (P(x)) 的证明。(plato.stanford.edu)
否定被理解为蕴涵荒谬： [ \neg A\equiv A\to\bot. ] 因此，证明 (\neg A) 意味着表明 (A) 的证明会导致矛盾，而不仅仅是说目前尚不知道 (A) 的证明。标准直觉主义逻辑保留了爆炸原理 (\bot\to B)，允许从荒谬推出任意命题。(cs.cornell.edu)
与经典推理的差异
排中律 [ A\lor\neg A ] 并不是直觉主义逻辑中的一般性定理。按照构造性解释，它要求对任意命题确立其中一个分支。不过，对于能够以构造性方式判定的命题，排中律仍然成立；不采用排中律，并不意味着断言它的每个具体实例都不成立。将排中律作为不受限制的公理模式加入，便可得到经典逻辑。(plato.stanford.edu)
同样，双重否定消去 (\neg\neg A\to A) 也并非普遍有效。表明“(A) 不可能成立”会导致矛盾的论证，不一定能提供 (A) 成立的证据。然而，(A\to\neg\neg A) 仍然有效。因此，反证法仍可用于确立一个否定命题：只要假设被否定的命题成立会导致荒谬即可；不能使用的是对由此得到的双重否定进行不受限制的消去。(plato.stanford.edu)
形式证明系统
直觉主义逻辑可以通过公理系统、自然演绎和相继式演算来表述。自然演绎为每个联结词规定了引入和消去的推理规则。例如，在假设 (A) 下推导出 (B)，就可以解除该假设并推导出 (A\to B)。蕴涵消去即肯定前件式：由 (A) 和 (A\to B) 推出 (B)。(cs.cmu.edu)
在标准的直觉主义相继式演算中，判断具有如下形式： [ \Gamma\vdash A, ] 其中，(\Gamma) 汇集各项假设，右侧则只有一个结论。这与经典相继式演算的多结论表述形成对比。这类系统为自动证明搜索和推导研究提供了结构化的方法。(cs.cmu.edu)
语义模型
在代数层面，直觉主义命题逻辑可在海廷代数中得到解释。海廷代数是带有蕴涵运算的有界分配格，该运算满足： [ c\le(a\to b)\quad\text{当且仅当}\quad c\land a\le b. ] 布尔代数是其特例，对应于经典逻辑。在一般的海廷代数中，一个命题与其否定的并不一定等于最大元。(mikeshulman.github.io)
一种具体的解释来自拓扑空间中的开集。合取对应交集，析取对应并集，否定则对应补集的内部。因此，双重否定不一定得到原来的开集。(mikeshulman.github.io)
克里普克语义则采用有序的信息阶段。一旦某个命题在一个阶段被强制成立，它在后续阶段也始终被强制成立。当每个强制其前件成立的后续阶段也强制其后件成立时，蕴涵便成立。关键在于，某个阶段未强制 (A) 成立，与该阶段强制 (\neg A) 成立并不相同。这些模型为直觉主义逻辑提供了可靠性和完备性结果。(plato.stanford.edu)
证明与计算
通过柯里—霍华德对应，命题对应于类型，证明对应于程序。蕴涵对应函数类型，合取对应积类型，析取对应带标签的和类型。将蕴涵的证明应用于其前件的证据，对应于函数应用。(cs.cmu.edu)
这一联系将直觉主义逻辑与类型论以及编程语言的设计关联起来。构造性的存在性证明包含见证对象，而析取命题的证明则包含一个已明确指出的分支。证明归约为逻辑推导提供了计算层面的解释，使推理系统能够将证据视为有结构、可执行的对象，而不仅仅是对真理的断言。(cs.cmu.edu)