判定問題

　　判定所謂“大量問題”是否具有演算法解，或者是否存在能行的方法使得對該問題中的每一特例能在有限步內機械地判定它是否具有某種性質（如是否真、是否可滿足或是否有解等，隨大量問題本身的性質而定）的問題。大量問題是與單個問題相對立的，它一般由無窮多個具有某種共性的單個問題組成。

　　上述“是否有演算法解”，“是否存在能行的方法”的說法中的“是”，指有演算法解或有能行的方法，這是不成問題的，因為憑人們的直觀至少在理論上總可以判斷一個解或一種方方法是算法解或是能行的方法，盡管有時它很長而且很復雜；但對其中的“否”即不存在算法解或不存在能行的方法，則問題要麻煩得多。這要求要有精確的“算法”概念或精確的“能行性理論”概念。後兩者在30年代才建立和發展起來，並成瞭“遞歸論”的基礎部分。有瞭精確算法概念之後，隨即發現許多長期懸而未決的大量問題不存在算法解，或者說是算法不可解的（根據丘奇論題，有時又說是遞歸不可解的），或者說該問題是不可判定的。其中最著名的有：①狹謂詞演算（也稱一階邏輯、一階函項演算等）公式的可滿足性的判定問題（A.丘奇，1936；A.M.圖靈，1937）；②群的字問題（∏.С.諾維科夫，1955；W.W.佈恩，1959）；③希爾伯特第10問題。

　　上述問題①就是希爾伯特所謂的“判定問題”。希爾伯特稱它是數理邏輯的基本問題或中心問題。如上所說，1936年已證明此問題不可解（指算法不可解）。但全體公式類的不可解並不蘊涵其子類的不可解性。事實上狹謂詞演算公式集的許多子類是有算法解的；當然也同樣有許多子類（特別是所謂“歸約類”）是不可解的。不妨把這方面的判定問題即由希爾伯特的“判定問題”所引伸出來的問題稱為“狹義的判定問題”，並把對於一般的大量問題的相應問題籠統地叫作“判定問題”。

　　狹義判定問題　狹謂詞演算公式的最簡單而且最著名的可判定子類是全體隻含一目謂詞的公式類（L.勒文海姆，1915；A.T.斯科朗，1919；H.伯赫曼，1922），以及如下的兩個前束類：

　　① 具有前束彐…彐∀…∀的前束公式類（P.貝爾奈斯、M.S.芬克爾，1928）；

　　② 具有前束彐…彐∀∀彐…彐的前束公式類（K.哥德爾，1932；L.卡爾馬，1933；K.許特，1934）。

　　在討論一階邏輯的不可解公式類之前先介紹“歸約類”的概念。簡單地說，它們是這樣的一些公式類，使得全體公式的判定問題能夠能行地化歸為這些類的判定問題。這方面最早和最簡單的情形是隻包含二目謂詞變元的公式類(勒文海姆，1915)以及具有前束∀…∀彐…彐的前束公式類（斯科朗，1920）。

　　由丘奇和圖靈的結果推出一切歸約類均為不可判定的。圖靈的證明是十分直截瞭當的。他用一階邏輯中的公式對圖靈機進行編碼，由此由圖靈機停機問題的不可解性便推出一階邏輯的不可判定性。

　　歸約法和編碼法仍是證明一階邏輯公式類不可判定性的兩個主要方法，利用歸約法可以證明如下公式類的不可判定性：

　　③ 具有前束∀∀∀彐的前束公式類（J.蘇拉尼，1950）。

　　利用對“鋪磚問題”進行編碼可證如下公式類的不可判定性：

　　④ 具有前束∀彐∀的前束公式類（A.S.卡爾，E.F.莫爾和王浩，1962）。

　　③和④中的公式類都是歸約類，而且可以看出公式類③為歸約類一事可以容易地由④中公式類的歸約性推出。不僅如此，有瞭④後許多有趣的歸約類都能十分容易地得到。

　　綜合①～④，如果不考慮等詞，則有如下結果，它表明對前束公式類而言可解與不可解的問題已經完全解決。

　　給定任何量詞串Q₁x₁，Q₂x₂，…，Q_kx_k，由此量詞串所確定的前束類是一個關於可滿足性的歸約類，當且僅當該量詞串包含∀彐∀或∀∀∀彐作為保持順序而不一定相連結的子串。每個不是歸約類的前束類都是可判定的。

　　如果單考慮公式中謂詞的目數和個數，則有如下結果，它在這方面可能是最好的瞭。

　　⑤ 一切隻含惟一的二目謂詞變元R的公式的集是歸約類（卡爾馬，1936）。

　　狹義判定問題還有許多問題沒有論及。主要是未討論前束公式的母式的真值函數形式以及出現在原子子公式中的個體變元的順序等。

　　關於狹義判定問題的另一個重要結果，是由Б.Α.特拉赫堅佈羅特於1950年證明的，即一階邏輯中公式是否在一有窮個體域上可滿足是不可判定的。

　　一般大量問題的判定問題　又分為一階(或初等)理論的判定問題和其他數學判定問題。前者是指給瞭一個形式理論，要求判定屬於相應語言的任一語句σ能否由該理論推出，或等價地，σ是否在該理論的一切模型上為真。例如，G.皮亞諾算術理論PA和公理集合論中的ZF系統都是不可判定的一階理論的例子，而實閉有序域或代數封閉域的一階理論則是可判定的一階理論的兩個例子。後者的例子也很多，如群的字問題（M.德肯，1911），丟番圖方程可解性的判定問題（希爾伯特第10問題，1900）等。

　　可判定理論的例子　以下對一數學結構或模型ц₀，令Th(ц)表一切在ц上真的語句組成的完備理論。

　　①Th(＜ω，≤＞)（C.H.蘭福德，1927；其中ω表全部自然數的集合）；

　　②Th(＜Q，≤＞)（蘭福德，1927；其中Q表全體有理數的集合）；

　　③Th(＜ω，+＞)，（M.普雷斯伯格，1929）；

　　④Th(＜R，0，1，+，·，≤，＞)（A.塔爾斯基，1948；其中R表一切實數的集合）；

　　⑤ 代數封閉域的初等理論（塔爾斯基，1948）；

　　⑥ 交換群的初等理論（W.什米萊夫，1954）；

　　⑦ 佈爾代數的初等理論（塔爾斯基，1940）。

　　以上諸理論的可判定性均可用消去量詞方法得到，而①～⑤情形的可判定性亦可用模型論方法得到。用模型論方法可證明其可判定性的理論還有：

　　⑧P進位域的初等理論（J.阿克斯和 S.B.科琴，1965～1966）；

　　⑨ 有限域的初等理論（阿克斯，1968）；

　　⑩ 線性（全）序集的初等理論（A.埃倫托伊希特，1959）。

　　情形⑧否定瞭長期懸而未決的如下猜想：除實閉域和代數封閉域外，沒有其他可判定的無限域。

　　證明理論的可判定性的方法除上面提到的消去量詞和模型論方法外還有解釋方法。情形③的可判定性就可用解釋方法證明。不過用解釋方法證明為可判定的理論大都是二階的。

　　不可判定的理論　丘奇1936年用哥德爾1931年證明不完備性定理的想法首先證明瞭皮亞諾算術理論PA（及其若幹子理論）為不可判定的。J.B.羅塞同年證明PA的任何無矛盾擴張均為不可判定的。塔爾斯基稱這樣的理論為本質不可判定理論。這種證明不可判定性的方法叫做直接方法。用直接方法能證明其不可判定性的理論應當充分強，使得數論的推理工具能在其中發展。還有一種間接方法，即歸約方法，其要點在於，把一理論T₁的判定問題歸約到一不可判定的理論T₂，由此證明T₁亦為不可判定的。這裡又分兩種情形：①證明T₁由T₂刪去有限條公理而得，丘奇正是用這一方法於1936年證明一階邏輯為不可判定的。②證明某一本質不可判定理論T₂可以在T₁中解釋。采用PA作為本質不可判定理論T₂，可證明各種公理集合論系統為不可判定的。

　　上述間接方法的適用范圍仍是有限的。還有一種廣義間接方法，它把上一方法中的兩種情形①、②的某些特點結合起來。這就是說，為瞭證明理論T₁不可判定，隻須把一有窮可公理化的本質不可判定理論T₂在T₁的某一無矛盾擴張中解釋即可。此種理論T₂自然不能沿用PA，因後者是不可有窮公理化的。下面的魯賓孫系統Q適合一切要求，其公理隻有7條

\ n

\ n

\ n

\ n

\ n

\n

用這種廣義間接方法已證明：群、環、域和格的初等理論均是不可判定的。還可證明，各種類型的群、環、域和格的初等理論的不可判定性。R.M.魯賓孫還用這些方法證明瞭許多特殊環 R的完備初等理論 Th( R)為不可判定的。此種環稱為不可判定的環。

　　不可解的問題　大批不可解的問題屬於組合判定問題，其中較有意義的是半群的字問題(A.圖埃，1914)和群的字問題。前一問題已證明為不可解的（E.L.波斯特，1947；Α.Α.馬爾可夫，1949）。群的字問題則要困難得多。如前面所說它的不可解性已由諾維科夫和佈恩在50年代相互獨立地證明。值得指出的是G.希格曼1961年證明瞭如下定理。

　　希格曼定理　一個群是遞歸可表示的當且僅當它同構於一有限呈示群的子群。

　　這個定理表明遞歸可表示這一遞歸論概念等價於一純代數概念。群的字問題的不可解性是它的一個容易的推論。

　　另外兩個有名的不可解問題是分屬於拓撲學和數論的問題：

　　①1958年證明維數≥4的流形同胚問題不可解（二維情形已由（G.F.）B.黎曼解決；三維流形的問題尚未解決）；

　　② 關於丟番圖方程可解性的判定問題(即希爾伯特第10問題)已於1970年最後否定地解決。

　　無論是狹義判定問題還是一般判定問題，在可解的情形有一個算法復雜性或可行性問題，對不可解的問題，則有一個不可解度的問題。

　　

參考書目

　A.Tarski，et al.，Undecidable Theories，Humanities Press，New York，1953.

J.Barwise，ed.，Handbook of MatheMatical Logic，Horth Holland，Amsterdam，1977.

　B.Dreben and W.D.Goldtarb，The Decision Problem Solvable Classes of Quantificational Formulas，Addison Wesley，Reading，Mass.，1979.