历史和哲学背景

数理逻辑与自动计算机之间常听人说起的联系有两点，一是可以用序列布尔函数表示计算机的基本构成单元，二是编程语言和逻辑符号系统很相似。因此无论是对于计算机的制造，还是对于计算机的使用，适当了解逻辑都是必不可少的。

逻辑和计算机之间的一个更基本的联系也许是对算法的共同兴趣。逻辑学家们不仅对算法进行了十分成功的抽象研究，还澄清了机器与算法之间的关系，后者主要是通过图灵的理想机器理论实现。

逻辑学家对形式化的关注是逻辑和计算机密切联系的最深层根源。数学证明形式化的追求经过了漫长的演化，最终导致机械化成为判断是否完全成功的终极标准。希尔伯特等人研究元数学：证明理论和形式系统理论。

正是对证明论的关注，首先引导艾尔布朗将计算过程抽象地定义为一种特别简单的证明类型。给出一个一般的算法定义，对这个问题的惊人简单的解决，无疑是关于计算的抽象研究迅速发展的一个重要原因。

在工程学和数学之间

逻辑是数学和哲学的混血儿；而实际计算机的诞生则是一件工程学伟绩。这一起源上的分歧带来了严重的科学难题。

科学方面的问题在于，大多数有雄心的人都觉得枯燥琐碎的工程学和无聊的智力训练一样令人厌恶。此问题的源头可以往回追溯很远。应用数学的每个分支都有一个内在的困境：每一项成果都是要么没有充分的应用，要么不够数学。

如果不考虑速度和潜无穷长纸带的问题，图灵机和实际计算机等价。图灵机还有其他一些配置形式，它们更接近于实际的计算机，例如用包含少量基本指令的程序表示的图灵机。

既然图灵机上存在不可解的问题，在实际计算机上，相应问题也是不可解的。擦除功能理论上对图灵机并非不可或缺。因此磁带（相比于纸带）在理论上不是制造计算机所必需的。

不可解问题

逻辑学家们熟知的一点是，所有数学理论都可以在初等逻辑的框架内进行表述。因此如果我们能一般地判定一个陈述是不是一个逻辑定理，我们就一样能判定一个陈述是否在某个给定的数学理论中可证。这一事实解释了为何希尔伯特学派将判定问题，即判定一个逻辑陈述是不是定理的问题，视作逻辑学的主要问题。

波斯特提出的一个问题仍未被解决。考虑所有由0和1构成的有穷字符串。如果一个串以0开头，就删掉其开头的三个字符并在其末尾处添加上00；如果它以1开头，就删掉其开头的三个字符并在其末尾处添加上1101；如果字符串包含的字符少于三个，就停下来。我们有没有一个一般的方法来判定，对于任意的两个字符串，其中第二个是否可由第一个通过上述规则得到？

如果将可解性等同于乘积系统或其他某种等价方法（比如图灵机）下的可解性，波斯特的方法就可用来建立一些否定性结果。图灵就提出并论证了这样一个等同，并应用关于图灵机的结果证明了判定问题不可解。

在其他数学分支中的一个应用是诺维科夫关于群的字问题不可解的证明，这个结果被马尔科夫用来证明四维同胚问题是不可解的。三维同胚问题仍然是一个开放问题。

马蒂埃西维奇证明了希尔伯特第十问题不可解：不存在判定整系数多项式方程有无整数解的普遍方法。因此对于有加法和乘法但无量词的数论，不存在判定程序。

不可解问题的一个形式上简单的例子是如下字问题。考虑由a、b、c、d、e五个符号构成的符号串和以下七条互换规则：ac↔ca，ad↔da，bc↔cb，bd↔db，adac↔abace，eca↔ae，edb↔be。判定任意两个字是否根据这些规则是等价的，这是一个不可解的问题。如果我们把第五条规则中的e换成c，则所得系统的字问题是可解的。

形式化

不可解结果属于理论方面，而个别数学证明的形式化或从逻辑推导数学，则属于实践方面。在后一方面，逻辑与计算机的互动在一个更具体的层面上意义重大：逻辑学的发展与实际计算机的强大能力结合在一起，给我们带来了数学证明机械化的希望，这不只是在原则上，而且是在实践上。

对机械化的兴趣意味着形式逻辑的重新定位，它要更追求效率。对公理和初始概念节俭性的要求需补充以对大量概念和规则的准确阐述，这些概念和规则构成普通数学家的工具库。

假设我们想证明：（*）x>1→∃y(Py∧(y|x))，即每个大于1的整数都有一个素除数。假设已经给定了一个有组织的信息库SF，其中首先列出的是+、·、<的性质，然后是P和|的性质。

基本的证明策略是假设该定理为假，进而尝试从最小的反例导出一个矛盾，这体现了数学归纳法原理的一个机械上方便的形式。所设想的最小反例构成一个“不明确的常项”，它不仅具有所有整数都有的普遍性质，还具有源于“它是一个反例”这个假设的特别的性质。在像（*）这样的简单情况下，援引SF中的信息并使用一些简单的真值函项演绎后，我们很快能得到一个具有矛盾性质的不明确的常项。

为了证明（*）,我们首先假设它为假，并令m为其最小反例：（1）m>1；（2）Pb→b∤m；（3）1

我们用m替换上面的a和b：（4）Pm→m∤m；（3）1

查阅SF找到P的定义性质并应用到m上：Pm↔∃x(1

用xm替换目前已得的一般陈述即（2）和（3）中的自由变项：（9）Pxm→xm∤m；（3）1

从（1）、（2）、（3）、（6-10）推导真值函项后承（先不使用SF）：（11）¬Pxm，根据（8）和（9）；（12）Pyxm，根据（7）和（10）；（13）yxm|xm，根据（7）和（10）。

现在利用SF中的信息(a|b)∧(b|c)→(a|c)：yxm|m，根据（8）和（13）。用不明确常项先替换（2）和（3）中的自由变项：（15）Pyxm→yxm∤m；（16）1

在实际编写一个机器程序之前，需要更准确地规定这个方法。但上述提纲表明，在现有机器上可以写出相当自然的程序来证明像（*）这样的定理。