什么是停机问题？

停机问题问每台图灵机是否会停机。这里假定图灵机是从一个空的纸带开始。图灵证明，对于每个个别的图灵机T，该问题总可以用谓词演算的一个个别语句F来表达，使得T会停机当且仅当F是不可满足的。因此假如有一个判定程序能判定谓词演算全部语句的有效性（或可满足性），停机问题就是可解的。

图灵的结果已经被改进到这个地步：我们需要的全部语句都具有相对简单的形式∀x∃y∀zMxyz,其中M不含任何量词。因此甚至对于谓词演算的∀∃∀语句构成的这个简单的类，判定问题也是不可解的。证明这一点的方法还产生了一个程序，它使我们可以将谓词演算的每一个语句与一个那种简单形式语句相关联。这样∀∃∀语句就构成一个“还原类”。还存在其他多种还原类。