Wiki. 直觉主义逻辑 [直觉主义逻辑]

观念

直觉主义逻辑又称构造主义逻辑 (constructive logic), 其核心观念是: 要接受一个命题为真, 必须给出它的一个例子.

例如, 要证明 $p \lor q$ ($p$ 或 $q$) 为真, 必须要么证明 $p$, 要么证明 $q$. 一个重要的后果是我们不能在不了解一个命题 $p$ 的前提下接受排中律 $p \lor \neg p$, 因为我们可能既不能证明 $p$, 也不能证明 $\neg p$.

要证明 $\exists x P(x)$, 必须给出一个具体的 $x$ 以及 $P(x)$ 的证明.

性质

模型

直觉主义命题演算的模型 (范畴语义) 是 Heyting 代数.

不可证命题列表

注意, 如下命题在直觉主义逻辑中不能证明, 但这不意味着它们的否定为真.

• 排中律 $p\lor\neg p$
• de Morgan 律 $\neg (p\land q) \Rightarrow (\neg p \lor \neg q)$