超小小中大超大

直觉主义逻辑（一） (6-1)

好书推荐：数学联邦政治世界观、万人迷被强制爱的日常、惊世狂妃：皇叔一宠到底、高冷冥夫宠上身、潜执CP（自创版）、穿书炮灰女配要修仙、万人迷omega被疼爱了、黑化徒弟萌宠师、我的神宠、幻境：多元宇、

何为逻辑？斯坦福哲学百科全书的 Logic and Ontology 条目给出了逻辑的四种常见的概念：

• 对于人工形式语言的研究

• 对于形式有效的推理和逻辑结果的研究

• 对于逻辑真的研究

• 对于判断的普遍特征或形式的研究

这四种概念在特定的研究场景下表现出极强的一致性，在另一些场景下则表现出明显的不同。

最为著名的“经典逻辑（classical logic）”是学习逻辑的一个起点，以及其他逻辑作为参照的标杆。经典逻辑侧重“真值”，陈述的“真值”是其“绝对”特征。一个无歧义的合式陈述（well-formed statement）或真或假。假即非真，真即非假，是为“排中律”（Law/principle of excluded middle,tertium non datur）。

基于经典逻辑，我们可以“非构造地”证明一个命题。例如：

∃x，y ∈ ℝ – ℚ s.t xʸ ∈ ℚ（存在两个无理数 x，y ，使得 xʸ 为有理数）。

证明：如果√2√2 是有理数，那么我们可以取 x＝y＝√2 ，否则可以取 x＝√2√2，y＝√2 .

上面的证明虽然在经典逻辑里没有问题，但我们仍无法确定究竟哪一种情况是正确的。除此之外，我们还可以做出一个构造性证明（constructive proof）：对于x＝√2，y＝2log₂3 ，我们有 xʸ＝3∈ℚ .

这种“构造式”的推理方式对应着“直觉主义逻辑”（intuitionistic logic）。直觉主义逻辑的哲学基础是，不存在绝对真理，只存在理想化数学家（创造主体）的知识和直觉主义构建。逻辑判断为真当且仅当创造主体可以核实它。所以，直觉主义逻辑不接受排中律。

BHK释义（The BHK interpretation）

直觉主义命题逻辑，或称直觉主义命题演算（Intuitionistic propositional calculus, IPC），的语言和经典命题逻辑的语言是一样的。

定义1

假设一个命题变量（propositional variables，或译为变项，为了保持逻辑、数学用语的一致性，类型论驿站中一般采用数学翻译法）无限集合PV，我们定义逻辑式（formulas）的集合 Φ 为满足下列条件的最小集合：

• 所有谓词变量和常量 ⊥ （谬）都是 Φ 的元素；

• 如果 ф，ψ∈Φ ，那么 (ф → ψ)，(ф∨ψ)，(ф∧ψ)∈Φ.

变量和常量被称为原子式（atomic formulas）。子式（subformula）是一个逻辑式（不一定平凡）的构成逻辑式。