本質不可判定性(essential undecidability)是一個不可判定的數學理論。若一個數學理論T是不可判定的，且其任意無矛盾擴張也是不可判定的。則稱其為本質不可判定的。
基本介紹
- 中文名：本質不可判定性
- 外文名：essential undecidability
- 領域：數學
- 學科：數學邏輯
- 性質：數學理論
- 特點：不可判定
概念,不可判定數學理論,算術系統的不可判定特性,判定問題,數學邏輯,
概念
本質不可判定性(essential undecidability)是一個不可判定的數學理論。若一個數學理論T是不可判定的，且其任意無矛盾擴張也是不可判定的。則稱其為本質不可判定的。本質不可判定的概念和思想對證明許多數學理論的不可判定性有很大作用。如果能證明某一本質不可判定理論T′可在理論T中解釋，則可知理論T是不可判定的。本質不可判定理論的最基本的一個例子是佩亞諾算術系統。
不可判定數學理論
不可判定數學理論是不具有能行判定算法的數學理論。對於語言L上的理論T，如果不存在一個能行的算法，使得對於L中的任何語句σ，該算法可以判定“σ∈T”是否成立，則稱理論T是不可判定的。最早被證明為不可判定的數學理論是佩亞諾算術PA(該問題是美國數學家、邏輯學家丘奇(Church，A.)於1936年證明的)，實際上，PA的任何無矛盾擴張都是不可判定的(如各種公理集合論系統就是不可判定的)。目前已知下列數學理論是不可判定的：
1.Th(〈z，+，·〉) (z為整數集)。
2.Th(〈Q，+，·〉) (Q為有理數集)。
3.群理論。
4.半群的理論。
5.環的理論。
6.域的理論。
7.格的理論。
8.分配格的理論。
9.偏序理論。
算術系統的不可判定特性
佩亞諾算術系統的不可判定特性。1936年，美國數學家、邏輯學家丘奇(Church，A.)用哥德爾證明不完備定理的思想證明了佩亞諾算術的不可判定性。美國學者羅塞(Rosser，J.B.)同年證明了佩亞諾算術是本質不可判定的。。由算術系統的本質不可判定性還可以得到諸如ZF系統等重要理論的不可判定性。
判定問題
判定問題是數理邏輯中的一個重要問題。它表現為尋求一種能行的方法、一種機械的程式或者算法，從而能夠對某些問題中的任何一個在有窮步驟內確定是否具有某一特定的性質。例如，命題邏輯的任一公式是不是常真這個問題，就可以在有窮步驟內按照一定的程式用真值判定。如果對某些問題已經獲得這種能行的方法，就說明這類問題是可判定的;如能夠證明某類問題不可能存在這樣的方法，就說這類問題不是能行可判定的。判定問題有不同的陳述。從語義方面考慮，判定問題是要確定一公式是否常真，亦即是否普遍有效;在語法方面，它是要確定某一公式是可證，還是可否證。從計算複雜性方面對可解的判定問題的研究證明，一些理論雖然原則上是可判定的，但它的判定程式(算法)所需的計算步數太大，以致在實踐上是不可行的。一個重要的問題是：是否存在某些可判定的理論。而且其判定方法是快速的，在實踐上是可行的，對於這個問題迄今未能作出肯定的或否定的回答。70年代以來，通過研究命題邏輯的判定方法的複雜性，發現了許多已知的組合型的判定問題都可化歸為命題邏輯的判定問題，如果能找到判定命題邏輯中的公式是否為重言式的快速算法，則可隨之而獲得一大批判定問題的快速算法。但迄今這仍是懸案，即未能找到命題邏輯的快速判定算法，也未能證明不存在它的快速判定算法。
數學邏輯
或稱數學邏輯、符號邏輯，是從思維的量的規定性來研究正確思維的形式和規律的科學(這裡所說的“量”，是哲學範疇的“量”，是最廣義的“量”，所指包括全部數學的對象)。數理邏輯在其發展的初期，只被看成“邏輯代數”，在形式邏輯中引進變數和方程式，用方程式的計算來代替推理，把形式邏輯當作代數系統來處理。後來人們才意識到數理邏輯對於數學的意義，開始把它套用於數學的奠基問題。數理邏輯和傳統的形式邏輯並不是對立的，它是以傳統的形式邏輯作為自己的基礎發展起來的，到了今天，也仍然是一般邏輯的一個特殊的分支。數理邏輯的主要研究對象是數學證明，而要研究數學證明，必須首先把證明的概念精確化，才能正確地陳述無矛盾性、完全性及判定性等問題，從而加以解決。其基本方法，是證明的形式化。它的要點如下;首先使用特殊的符號，即除平常的數學符號以外，還要把數學中所常使用的聯結詞，如“與”、“或”、“如果……那么”、“不”等等，以及其他的邏輯詞項，用特殊的符號來表示，把所發展的理論中的定理和公理的陳述都寫成公式的形式，把理論符號化。符號化以後，由公理推演定理，或者說定理的證明就變成公式的演算，從已有的公式推演出新的公式。這樣一來，證明，或者說是推演，就成為一連串的公式，其中最後的公式就是所要推演的公式。數理邏輯與電子計算機的構造理論有著深刻的聯繫。數理邏輯可以套用於各種訊息處理系統。
