直觉主义逻辑 (3-2)

A proof of A∧B is a pair comprising a proof of A and a proof of B.

A proof ofA∨B is a proof of A or a proof of B.

A proof of ⇁ A is a proof that there is no proof of A.

A proof of A ⊐ B is a construction that, given any proof of A， can be applied to give a proof of B.

A∧B 为真表示存在A和B的证明，A∨B为真表示A或B中至少有一者存在证明，⇁ A为真表示“可以证明’不存在A的证明‘”.A ⊐ B为真表示，给出A的证明，可以导出B的证明

就像我们现在，既无法证明孪生素数定理(A)，又无法证明我们不能证明孪生素数定理(⇁ A).在这种情况下，A∨⇁ A为假。

可能世界语义(Possible-World Semantics)下的直觉主义逻辑

如果我们采用可能世界语义(Possible-World Semantics)，在这套语义下，我们有若干个世界，一个命题在任意一个世界中，要么是真的，要么是假的。每一个世界可以看到(see)某些另外的世界。世界的集合记作W，这种看见的二元关系记作R（ωRω'表示世界ω看见世界ω'）。我们可以引入一个赋值函数υ，υω(p)＝1表示世界ω中命题p被赋值真。如此我们就有一个结构：〈W，R，υ〉，即世界的集合、世界的关系、世界中命题的赋值函数组成了一个结构。

在一个世界ω中，如果它看到的所有世界ω'都有p成立，那么在这个世界ω中，有□p。如果它看到的世界中，存在ω'使得在ω'中p成立，那么记作♢p。

那么我们用这套语言来重构直觉主义逻辑。

怎么定义世界？一个世界ω与它的赋值函数υω紧密相关，其中υω给每一个命题p赋值。一种赋值方式，就是一个世界。在直觉主义逻辑这里，一个世界ω，就是一种赋值方式υω，υω给每一个命题赋值，如果这个命题可以证明，则被赋值1，若无法证明”这个命题可以证明“，则被赋值0。

怎么定义关系“看到”？一个世界ω可以“看到”另一个世界ω'，则ω'解决了ω的中一些无法证明的问题，也就说，ω'要么是ω，要么是ω的理论体系的进一步的发展。用数学符号来理解，就是：

对任意ω ∈ W，如果υω(p)＝1而且ωRω'，那么υω'(p)＝1

这被称为遗传条件(Heredity Condition)这种二元关系R满足自反性和传递性。

我们现在来看课本上的定义(Graham Priest[4])：

υω(A∧B)＝1 if νω (A)＝1 and νω (B)＝1；otherwise it is 0 .

υω(A∨B)＝1 if υω (A)＝1 or υω (B)＝1；otherwise it is 0 .

υω(A ⊐ B)＝1 if for all ω' such that ωRω' either or υω'(B)＝1；otherwise it is 0 .

那如何理解⇁ A的意思，即为□¬A。也就是说，在所有当前理论世界的进一步发展的理论世界中，都不可能有A，这等价于当前世界存在“A无法证明”的证明。

那在这套架构下，A ⊐ B，即为□(A ⊃ B)，即当前理论世界的任意一个进一步发展的理论世界中，都有A ⊃ B。

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。