判定(可解性)问题
由于形式化演绎理论的建立而产生的基本问题之一。 对于每一个具体的形式理论来说，判定问题的肯定解决或否定解决分别与某种一般方法(或算法)之存在或不存在有关。这种一般方法使我们有可能用有穷步的运算来弄清，所考察之理论的任何一个公式在该体系中是不是可证明的(真实的)。 例如在命题演算中和在亚里士多德的形式化的三段论法中，判定问题是能得到肯定解决的。但是对于谓词演算来说，就不存在对这一问题的一般解决。 不可能为某一形式理论找到一般的判定方法，这一事实并不排除可以为这一理论某类公式找到那样的解决办法。 |