《通往逻辑、数学和编程的Haskell之路》—— 一阶逻辑的形式和意义(1)

本篇的内容是关于书中第二章的内容，从计算的角度理解逻辑中的一些基本概念，例如，逻辑连接符的概念和意义，论证的有效性，逻辑学中的陈述性概念如何表示为计算中的算法概念，特别是对量词概念在计算中的再定义。
在前面的笔记中，曾经多次强调函数的重要性，这里再一次简明归纳一下：
函数的过程/映射二象性：一个函数，既可以看做是一个计算过程，也可以看做是两个集合之间的映射关系，前者又称作算法，或者函数内涵性的定义，后者称作函数的外延性定义。如果你是个程序员，可能马上理解我在说什么。在某些程序设计语言中（例如C语言），一个新的函数产生，要经过声明、定义和调用三个步骤。所谓‘声明’，就是只规定函数的接口：函数名，参数的个数和类型，以及返回值的类型。在这个阶段，我们无从知道这个函数具体内容，假定函数的参数个数为1，参数类型是整数，返回类型也是整数，那么，这个对函数的‘声明’实际上确定了函数的外延，亦即，整数集合到整数集合的映射关系：
ƒ：Z → Z
其中，ƒ代表函数名，Z是整数集合，箭头表示两个集合之间的映射关系。
在函数的‘定义’阶段，作为程序员，我们要严格、精确地描述函数的计算过程。这个过程必须是有限步骤可以完成的，完成后必须产生一个确定的结果。
最后是函数的‘调用’，将具体的对象带入到函数参数中，函数将返回一个确定的‘值’。由这个例子，我们可以有两个看待函数的视角：
静态的：只关心函数的输入和输出，亦即，集合之间的映射关系；
动态的：将函数看做是一个算法，一个由有限多个‘动作’完成的一个计算任务。
这两种看待函数的方式，我们称之为函数的“过程/映射二象性”。反之，无论是在哲学、数学、逻辑学还是计算机科学，凡是具备这种“过程/映射二象性”的对象，我们都可以称作函数。从哲学的角度来看，存在问题不再是思辨问题，不再仅仅是证明问题，而更是一个建构性的问题，只要你能够构造出要证明的对象，就可以确定其存在，而不仅仅是用反证法证明如果不存在将会导致矛盾。从数学角度，要证明某个数学对象具有某个性质，我们可以建立一个算法，例如，证明某个自然数是素数，我们可以通过有限步骤的算术运算，构造出这个数。从计算机科学的角度，我们可以编写个判定函数，经过有限次运算得到关于该自然数是否是素数的布尔值。以这种思想作为哲学、数学思想的学派，称作直觉主义，或者建构主义，这个学派的创始人是荷兰数学家布劳威尔(L.E.J. Brouwer)，而将其思想发扬光大的是布劳威尔的嫡传弟子荷兰数学家海廷(Arend Heyting)、英国哲学家达米特(Michael Dummett)，美国数理逻辑学家克里尼(Stephen Kleene)，以及法国数学家庞加莱(Henri Poincaré)。这一派数学哲学思想，在上个世纪60年代重新受到重视，是现代计算机科学的哲学思想之一。本书的作者基本上也是秉承这个思想，将逻辑学的基本概念、定义、定理都看做是一个可构造的算法过程。这一点也和我们前面引述的SICP的基本思想一致：计算机科学的本质是对陈述性、定义性知识的过程性再定义。见微而知著，从上面关于函数“过程/映射二象性”，我们也可以体会这个思想的基本要义。这个思想是我们今后学习的理论基础。
本章的内容分为6个小节：
1. 逻辑连接符的概念和意义
本节介绍了命题逻辑的5个逻辑连接符的使用、意义以及如何在haskell的解释器环境中实现。
2. 逻辑有效性和相关的概念
有效性是逻辑推理、论证和证明的主要概念，如何将有效论证转化为复合命题句的永真式，以及在haskell语言中实现的方法。
3. 变量的语义和量词概念
如何在逻辑的语境中理解变量的概念，以及变量和量词的关系
4. lambda抽象
本节引入lambda表达式的概念，以及lambda函数式的类型表达，介绍类型论的初步概念
5. 定义和实现
本节非常短，但提出了一个非常重要的问题：如何将一个数学命题转化为算法，亦即，将陈述性知识转化为过程性知识？
6. 抽象公式与具体结构
介绍逻辑式与数学对象之间的映射关系——公式与模型，这部分属于一阶逻辑的语义论。
7. 对量词的逻辑处理
介绍量词概念和带量词的命题
8. 作为过程/程式的量词
作为第5节和第6节原则的应用，学习如何将带量词的命题转化为算法过程。
下一篇，我们将详细介绍第1节和第2节的内容。请到官网下载第二章的Haskell源码：TAMO.hs以备下次内容之需。如果不知如何下载，可参考这篇文章。