类型系统和逻辑

计算机科学领域中一个重要成就是：类型理论type theory对应于一个特别的逻辑系统。Type systems and logic一文以Haskell语言为例详细介绍了其中细节：

那么这种对应到底是怎样的？其基本思想来自于Curry-Howard Correspondence. 一个类型被解释为一个命题proposition, 而一个值被解释为一个命题的证明proof， 大部分标准逻辑连接词都来自于这个思想。

举例来说：(A, B)的一对类型的值是类型A和B值的一对， 这意思是：它们是A和B的证明的一对，那就意味着(A, B)代表了逻辑连接词“A && B”.

同样类似，逻辑分离词disjunction (“A | | B”)代表一个所谓“标签联合tagged union”类型: A B两者中任何一个的值(证明) 是A的值(证明)或者是B的值(证明)。

类似 Int 和 String类型都是命题 – 你能认为像这些简单类型只是代表某种陈述：也就是“一个 Int存在” 或 “一个String存在”. 1是Int的证明, 而 "hands"是 String的证明. (Int, String) 是一个简单类型组, 陈述的是 “有存在一个Int和有存在一个String”，(1, "hands")是 (Int, String)的证明。

如果你不熟悉Haskell，Either类型会更加神秘一些, 类型Either a b 代表包含一个类型值出现在Either的左边，而类型b的值出现在Either的右边. 所以，Either Int String 意味着“可能存在一个Int或存在一个String”, 它被可能左边的1 或右边的"hands"证明了. 这种左右标签确保你在出现两个同样类型时，不会丢失任何信息。

如果两个类型相同，如：Either Int Int能被左边的1 或者右边的1证明, 这可以从它们彼此标签位置来进行区分。

当你思考蕴涵逻辑implication时会更加有趣. 函数的类型是转换类型A的值 (证明) 到类型B的值 (证明) ，也就是A -> B. 这意味着一个函数是也一个证明，这个证明代表：无论什么时候有一个A的证明，你都能得到B的证明，“如果A是真，那么B是真”(“if A is true, then B is true.”) ，这样函数是一种代表关系的蕴涵逻辑的证明。

有一件事比较奇怪，代表“not A”的命题是使用类型 A -> ⊥, 这里字符“ ⊥ ”被称为一个空类型，所谓空类型也就是没有值的类型，(类型的符号来自于数学，它通常代表明确的 “bottom.”含义)， A -> Void可以被读作：“如果我们有一个A, 我们能用它做些不存在的事情” –相对“我们并没有一个A”，这有一个很大的延伸，这好像是一种否定句，但是有一个问题: 在经典逻辑中，否定是可逆的reversible. 你能说“not (not A),” 经典逻辑认为那等同于说“A.”

看来经典逻辑是正确的 – 如果A不是假, 它一定是真, 对吗? 但是如果我们使用 A -> Void 作为否定的定义, 我们通常的直觉和经典逻辑规则就Hold不住了，一个类型(A -> Void) -> Void的值并不会让你得到一个 类型A的值，双否定不等同于正肯定了，这意味着什么？

这里其实代表了范式切换，.类型系统并不对应经典逻辑, 而是对应一种称为“constructive logic(构造逻辑)”. 这个范式切换是这样：我们从思考一个事物是否是真， 切换到我们是否能够证明它们，更重要的是，我们不再考虑是否存在等量化词(existential quantifications )，除非它被一个案例证明。

我们不能通过矛盾contradiction来证明， (比如：“至少肯定存在一个蓝色的事物，因为如果没有，那么我们就有矛盾了”). 相反，如果我们展示某个事物一些属性的存在，我们就能够发现这个事物，(“至少肯定存在一个事物，这个细节已经表明”). 只要我们记住我们的逻辑模型是可证明的，而不是单纯的真理(banq注：单纯的真理代表灌输：我就是比你强，我说的话就是真理，没有我就没有你们，这些都是单纯的真理，你只要记住就可以，无需知道如何证明它们，它们是怎么得出的)。

让我们重新考虑“not (not A)”这个案例，在构造逻辑constructive logic中 , 一个 A -> Void的证明, 或者 “not A,”的证明，是一个机制，其将获取一个 A，不能做任何事，返回了命题"false"的证明，如果你有一个实际的假false的证明 (比如如果你既有一个 A 和一个 A -> Void 同时满足), 那就很坏: 在大多数逻辑中，你能用这个不可能逐个证明其他任何事，所有陈述都是等同，它们都是true且false。如果你将逻辑自身作为一个小宇宙，那么在那里逻辑规则就是物理规律，那么你可以说一个假false的证明会摧毁这个小宇宙，将黑洞会吸入整个宇宙到一个单点。

那么，回到not A. 大部分我们感兴趣的逻辑是“一致性consistent”, 其基本意思是那是不可能摧毁整个宇宙的。那么， A -> Void 意味着 “如果你给我一个 A, 我会摧毁整个世界” – 也就是说，如果我们用一致性逻辑，我们证明了 A -> Void, 我们知道就不可能证明A. 这样 A -> Void 似乎只能是我们预期的not A 的意思.

最后，回到双否定，如果 not A 是 a -> Void, 那么not (not A)就是 (A -> Void) -> Void, 或者 “如果你给我一个机器，获得输入A，并摧毁整个世界，那么我也将摧毁整个世界.” 但是这其实不会给你一个A，如果你关心一些不可触及的真理概念，你会肯定将这个概念应用到A，但是以我们构成主义的逻辑来说，我们现在不感兴趣真相，我们只感兴趣为什么(As)。

双否定的离奇怪异来自于排中律(the Law of the Excluded Middle) – 对于任何命题“A”, 或者 “A”是真或者“not A”是真 – 但这并不符合构造逻辑(constructive logic).

当你谈论抽象的真理时，很显然，任何命题要么是真要么是假，但是涉及证明时 – 你能建立吗？你能建立一个没有任何信息的盒子，当你输入一个类型A的值时，它要么是类型A的值，要么是一个摧毁世界的机制？至少我不能，许多经典逻辑规则在你只思考“真理”这个抽象概念时是很明显正确的，但是当我们从“可证明”角度考虑时很显然没有意义了。

....