直觉主义逻辑

直觉主义逻辑或构造性逻辑是最初由阿蘭德·海廷开发的为鲁伊兹·布劳威尔的数学直觉主义计划提供形式基础的符号逻辑。这个系统保持跨越生成导出命题的变换的证实性而不是真理性。从实用的观点，也有使用直觉逻辑的强烈动机，因为它有存在性质，这使它还适合其他形式的数学构造主义。

语法 [编辑]

Rieger-Nishimura 格。它的節點是上至直覺邏輯等價的一元命題公式，按直覺邏輯蘊含排序。

直觉逻辑的公式的语法类似于命题逻辑或一阶逻辑。但是直覺邏輯的連結詞不像經典邏輯那樣是可互定義的，因此它們的選擇是重要的。在直覺命題邏輯中通常使用 →, ∧, ∨, ⊥ 作為基本連結詞，把 ¬ 作為 ¬A = (A → ⊥) 的簡寫處理。在直覺一階邏輯中量詞 ∃, ∀ 都是需要的。

不同在于很多经典逻辑的重言式在直觉逻辑中不再是可证明的。例子不只包括排中律 P ∨ ¬P，还有皮尔士定律 ((P → Q) → P) → P，甚至还有双重否定除去。在经典逻辑中，P → ¬¬P 和 ¬¬P → P 二者都是定理。在直觉逻辑中，只有前者是定理: 双重否定可以介入但不能除去。

对很多经典有效重言式不是直觉逻辑的定理的观察导致了弱化经典逻辑的证明论的想法。

相继式演算 [编辑]

主条目：相继式演算

根岑发现简单限制他的系统 LK (他的经典逻辑的相继式演算)就导致了关于直觉逻辑的一个可靠和完备的系统。他称之为系统 LJ。

希尔伯特式演算 [编辑]

推理规则是肯定前件，公理有:

THEN-1: φ → (χ → φ)
THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
AND-1: φ ∧ χ → φ
AND-2: φ ∧ χ → χ
AND-3: φ → (χ → (φ ∧ χ))
OR-1: φ → φ ∨ χ
OR-2: χ → φ ∨ χ
OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
NOT-1: (φ → χ) → ((φ → ¬χ) → ¬ φ)
NOT-2: φ → (¬φ → χ)

对于一阶逻辑系统还要加上普遍化规则，和如下公理:

PRED-1: (∀x Z(x)) → Z(t)
PRED-2: Z(t) → (∃x Z(x))
PRED-3: (∀x (W → Z(x))) → (W → ∀x Z(x))
PRED-4: (∀x (Z(x) → W)) → (∃x Z(x) → W)

算子的不可互定义性 [编辑]

在经典命题逻辑中，有可能选取合取、析取或蕴涵中的一个作为原始的，并依据它和否定来定义另两个，比如在扬·武卡谢维奇的命题逻辑三公理中。甚至可以依据自足算子比如皮尔士箭头(NOR)或Sheffer竖线(NAND)定义它们四个。类似的，在经典一阶逻辑中，一个量词可以依据另一个量词和否定来定义。

这是二值原理的推论，它使得这种连结词仅仅是布尔函数。二值原理在直觉逻辑中不成立，只有无矛盾律成立。作为结果没有连结词可以豁免，而上述公理都是必须的。多数经典恒等式只是直觉逻辑中在一个方向上的定理，尽管某些定理是两个方向的。它们如下:

合取与析取:

$(\phi \wedge \psi) \to \neg (\neg \phi \vee \neg \psi)$
$(\phi \vee \psi) \to \neg (\neg \phi \wedge \neg \psi)$
$(\neg \phi \vee \neg \psi) \to \neg (\phi \wedge \psi)$
$(\neg \phi \wedge \neg \psi) \leftrightarrow \neg (\phi \vee \psi)$

合取与蕴涵:

$(\phi \wedge \psi) \to \neg (\phi \to \neg \psi)$
$(\phi \to \psi) \to \neg (\phi \wedge \neg \psi)$
$(\phi \wedge \neg \psi) \to \neg (\phi \to \psi)$
$(\phi \to \neg \psi) \leftrightarrow \neg (\phi \wedge \psi)$

析取与蕴涵:

$(\phi \vee \psi) \to (\neg \phi \to \psi)$
$(\neg \phi \vee \psi) \to (\phi \to \psi)$
$\neg (\phi \to \psi) \to \neg (\neg \phi \vee \psi)$
$\neg (\phi \vee \psi) \leftrightarrow \neg (\neg \phi \to \psi)$

全称量词与存在量词:

$(\forall x \ \phi(x)) \to \neg (\exist x \ \neg \phi(x))$
$(\exist x \ \phi(x)) \to \neg (\forall x \ \neg \phi(x))$
$(\exist x \ \neg \phi(x)) \to \neg (\forall x \ \phi(x))$
$(\forall x \ \neg \phi(x)) \leftrightarrow \neg (\exist x \ \phi(x))$

所以，例如 “a 或 b”是比“如果非 a 则 b”更强的陈述，而在经典逻辑中它们是可互换的。

據 Alexander Kuznetsov 的證明，任一下述定義的連結詞可以充當直覺邏輯的自足算子:^[1]

$((p\lor q)\land\neg r)\lor(\neg p\land(q\leftrightarrow r)),$
$p\to(q\land\neg r\land(s\lor t)).$

语义 [编辑]

语义要比经典逻辑更加复杂。其模型论可给出自海廷代数或等价的给出自克里普克语义。

海廷代数语义 [编辑]

在经典逻辑中，我们经常讨论一个公式可能接受的真值。这种值通常被选择为布尔代数的成员。在布尔代数中的交和并算子等同于 ∧ 和 ∨ 逻辑连结词，所以形如 A ∧ B 的公式是在布尔代数中 A 的值和 B 的值的交。所以我们就有了一个有用的定理，一个公式是经典逻辑的有效的句子/断定，当且仅当它的值对于任何求值都是 1---就是说，对它的变量的任何指派都是真。

对于直觉逻辑对应的法则也是真的，但是不再对每个公式指派(assign)来自布尔代数的值，而是使用来自海廷代数的值，布尔代数是它的特殊情况。公式在直觉逻辑中是有效的，当且仅当它对于在任何海廷代数上的任何求值总是得到值 1。

可以证实为了识别有效的公式，考虑其元素是实平面 R² 的开集的一个单一的 Heyting 代数就足够了。在这种代数中，∧ 和 ∨ 算子对应于集合的交集和并集，并且指派给公式 A→B 的值是 (A^C ∪ B)^o，它是 B 的值和 A 的值的补集的并集的内部。底元素是 ø ，顶元素是整个平面 R²。¬A 定义为 A→ø，所以指派给它的值是 A^C^o，这是 A 的值的补集的内部。通过这些指派，直觉上有效的公式正好就是被指派为整个平面的值的公式。

例如，公式 ¬(A ∧ ¬A) 是有效的，因为不管为公式 A 选择什么集合 X 作为值，¬(A ∧ ¬A) 的值总是被证实为整个平面:

Value(¬(A ∧ ¬A)) =

(Value(A ∧ ¬A))^C° =

(Value(A) ∩ Value(¬A))^C° =

(X ∩ (Value(A))^C°)^C° =

(X ∩ X^C°)^C°

一个拓扑学定理告诉我们 X^C°是 X^C 的子集，所以交集为空，因此:

ø^C° = (R²)° = R²

所以这个公式的求值是真，这个公式确实是有效的。

但是排中律 A∨¬A，可以被证实是“无效的”，通过设定 A 的值是 {y : y > 0 }。那么 ¬A 的值是 {y : y ≤ 0 } 的内部，它就是 {y : y < 0 }，而公式的值是 {y : y > 0 } 和 {y : y < 0 } 的并集，这“不”是整个平面。

上面描述的无限海廷代数对所有直觉上有效的公式给出了真求值，而不管为公式中的变量指派了什么值。反过来说，对于每个无效的公式，都有来对变量的来自这个代数的一个值指派生成这个公式的一个假求值。可以证实没有有限的海廷代数有这个性质。

克里普克语义 [编辑]

主条目：關係語義

建立在他关于模态逻辑的语义的工作之上，索尔·阿伦·克里普克为直觉逻辑建立了另一套语义，叫做克里普克语义或关系语义^[2]。

参见 [编辑]

注释 [编辑]

^ Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.
^ Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

引用 [编辑]

Van Dalen, Dirk, 2001, "Intuitionistic Logic," in Goble, Lou, ed., The Blackwell Guide to Philosophical Logic. Blackwell.
Morten H. Sørensen, Pawel Urzyczyn, 2006, Lectures on the Curry-Howard Isomorphism (chapter 2: "Intuitionistic Logic"). Studies in Logic and the Foundations of Mathematics vol. 149, Elsevier.

外部链接 [编辑]

Stanford Encyclopedia of Philosophy entry

[1] Alexander Chagrov, Michael Zakharyaschev, Modal Logic, vol. 35 of Oxford Logic Guides, Oxford University Press, 1997, pp. 58–59.

[Mosch-IntLog-2] Intuitionistic Logic. Written by Joan Moschovakis. Published in Stanford Encyclopedia of Philosophy.

[1]

[2]