判定問題
正文
數理邏輯中的一個重要問題。它表現為尋求一種能行的方法、一種機械的程式或者算法，從而能夠對某類問題中的任何一個在有窮步驟內確定是否具有某一特定的性質。例如，命題邏輯的任一公式是不是常真這個問題， 就可以在有窮步內按照一定的程式用真值表判定。如果對某類問題已經獲得這種能行的方法，就說明這類問題是可判定的，或者說其判定問題是可解的；如能夠證明某類問題不可能存在這樣的方法，就說這類問題不是能行可判定的。判定問題有不同的陳述。從語義方面考慮，判定問題是要確定一公式是否常真，亦即是否普遍有效，或者可否滿足；在語法方面，它是要確定某一公式是可證，還是可否證。邏輯系統的判定問題 命題邏輯的任一公式是否常真以及是否可證都是能行可判定的。20世紀30年代美國數學家A.丘奇和英國的A.M.圖林分別證明了謂詞邏輯的判定問題是不可解的。對謂詞邏輯公式可以用前束範式分類，前束範式是一公式，其中一切量詞都未被否定地處於公式的最前方，謂詞邏輯的每一公式都和一前束範式等值或者可以互推。有些前束範式類是可判定的，例如只含有全稱量詞的前束範式。1962年A.S.柯爾、E.F.摩爾和美籍華人學者王浩證明了不可判定的謂詞邏輯公式都可以歸約為凬ヨ凬式。這種不可判定的公式類型被稱為歸納類。
在數學系統里，C.H.朗格弗德於1927年證明了自然數的線性序理論的判定問題是可解的。1929年，M.普利斯貝格證明了自然數的加法理論的判定問題是可解的。50年代初，A.塔爾斯基解決了初等幾何理論的判定問題。1970年，蘇聯學者Ю.В.馬季亞謝維奇證明了 D.希爾伯特所提出的23個著名數學問題中的第10個問題是不可解的。希爾伯特第10個問題是指尋找一個算法，用它能確定一任給的整係數多項式方程
p(x1,...,xn)=0
是否有整數解。結果證明，這樣的算法是不存在的。
證明一個理論的判定問題可解，只需給出一個算法，並證明這算法就是所要求的，問題就解決了。要證明一個理論的判定問題是不可解的，首先需要把算法（機械程式）概念精確化，並給出算法概念的嚴格的數學定義，使一切算法的類成為明確的數學對象，從而能用嚴格的數學方法證明對某個理論來說不存在解決它的判定問題的算法。判定問題的研究推動了對算法理論或稱可計算性理論的研究，促進了遞歸函式論（見遞歸論）和圖林機器理論的建立。
能行性和可行性 從計算複雜性方面對可解的判定問題的研究證明，一些理論雖然原則上是可判定的，但它的判定程式（算法）所需的計算步數太大，以致在實踐上是不可行的。例如，就可判定的自然數的加法理論來說，已經證明，對於該理論的每一判定算法，都有長度（即符號數目）為 n的語句（公式），使得依據該算法判定此語句是否可證需要計算 22cn步（c為>0的常數）。假如取n=10，那末即使使用每秒運算一億次的高速計算機作判定,也需要很多億個世紀。一個重要的問題是:是否存在某些可判定的理論。而且其判定方法是快速的,在實踐上是可行的。對於這個問題迄今未能作出肯定的或否定的回答。70年代以來，通過研究命題邏輯的判定方法的複雜性，發現了許多已知的組合型的判定問題都可化歸為命題邏輯的判定問題，如果能找到判定命題邏輯中的公式是否為重言式的快速算法，則可隨之而獲得一大批判定問題的快速算法。但迄今這仍是懸案，既未能找到命題邏輯的快速判定算法，也未能證明不存在它的快速判定算法。
