# Intuitionistic Logic

> 【EN】Intuitionistic logic encompasses the general principles of logical reasoning which have been abstracted by logicians from intuitionistic mathematics, as developed by L. E. J. Brouwer beginning in his [1907] and [1908]. Because these principles also hold for Russian recursive mathematics and the constructive analysis of E. Bishop and his followers, intuitionistic logic may be considered the logical basis of constructive mathematics . Although intuitionistic analysis conflicts with classical analysis, intuitionistic Heyting arithmetic is a subsystem of classical Peano arithmetic. It follows that intuitionistic propositional logic is a proper subsystem of classical propositional logic, and pure intuitionistic predicate logic is a proper subsystem of pure classical predicate logic. … 【中】词条追溯直觉主义逻辑源自布劳威尔自1907年与1908年开始的直觉主义数学工作。由于这些原则对俄罗斯递归数学以及毕晓普学派的构造性分析同样成立，它被视为构造性数学的逻辑基础。直觉主义分析与经典分析相冲突，但直觉主义Heyting算术却是经典皮亚诺算术的子系统。词条还讨论对排中律的拒斥、可允许规则与实现性语义。

- ID: m13250
- Category: structure
- Domain: 逻辑学

## Definition

直觉主义逻辑是逻辑学家从布劳威尔自1907年、1908年起发展的直觉主义数学中抽象出的推理原则体系。这些原则同样适用于俄罗斯递归数学与毕晓普学派的构造性分析，故被视为构造性数学的逻辑基础。 脚手架作用：- 构造检验：要求给出具体见证才承认一条存在断言 - 判定自查：面对排中律式断言先问自己能否实际判定 - 程序转化：把证明看成可执行的构造步骤而非现成的真理

## How it works

直觉主义把真理解为可证明、可构造：A∨¬A 要求我们能判定 A 或判定 ¬A，而并非总有这种能力，故排中律失效；∃xA(x) 要求能具体给出一个见证；否定与蕴含按证明之间的变换来定义，¬¬A 因此不等价于 A。

## Practice

1) 面对一个断言，先追问它的证明或构造是什么；2) 拆解证明：¬A 的证明就是把 A 的证明转化为矛盾；3) 拒绝无法判定的二者择一，改找可构造的替代路径。

## Use

- 构造检验：要求给出具体见证才承认一条存在断言 - 判定自查：面对排中律式断言先问自己能否实际判定 - 程序转化：把证明看成可执行的构造步骤而非现成的真理

[Read the web page](https://thinkingmodels.site/en/entries/detail/m13250)