根據獲“刻畫邏輯”的方法,命題變元的值限於“真”和“假”。近年來有些邏輯學家對此種觀點提出了疑問。
關於以古典方法刻畫邏輯的另一個有爭議的問題,是把直觀的“如果那麼”刻畫成“實質蘊涵”的問題。所謂實質蘊涵卬蘊涵隻)用符號表示就是礦,其涵義為“不能真而假”。從本世紀初期開始,許多邏輯學家就對這種解釋的可靠性提出懷疑。他們指出“如果那麼”這一直觀概念的某些重要的內容被“實質蘊涵”丟棄了。有人提出用“嚴格蘊涵”嚴格蘊涵礦是說真而假是不可能的,用符號表示,為來取代“實質蘊涵”。但由於嚴格蘊涵也會引起某些邏輯困難,所以“實質蘊涵”至今仍是表示“如果…那麼…”的標準形式。
麵所說的這些例子表明,目前對邏輯的“形式刻畫”可能並非定局。
三、集合論中的“形式刻畫”
最後,在這一節中我們討論一下目前計算機科學中正在采用的一些形式方法,從而有可能看到邏輯學家使用此種方法多年的經驗對計算機科學家當是有益的。
下麵,我們來考慮與形式語言和計算複雜性中所應用的方法有關的一些問題。
形式語言
作為程序語言的涵義理論的形式語言學,如所周知,有好幾種形式語言學,其中最重要的兩種是操作語言學和指稱語言學。在前者,是用抽象的機器來解釋程序的涵義;而在後者,則是用數學對象(比如可計算函數)來解釋程序的涵義。在某種意義上,用來解釋一個具體程序的——不管是抽象的機器還是可計算函數——都可以看作是對該程序的一種形式。一般說來,所謂一個具體語言的表達式的“形式涵義”,指的是一種形式語言中與之對應的表達式使得存在一個能行的映射。
這兩種語言學在效率方麵有所不同。對操作語言學而言,一個程序中的很多程序細節都被映人同一個抽象機器,因而在應用(例如編輯)時較為好使。其弱點在於,從數學角度看有時顯得有些笨拙。指稱語言學從數學上看既簡潔又優美。其弱點是應用起來不夠好使。其餘的語言學大體上介乎這二者之間。
計算複雜性理論
計算複雜性理論的核心問題之一是對“實際可計算性”一一即“在現實機器上的可計算性”也叫“可行性”這一直觀概念的“形式刻畫”。有關研究人員目前所采用的形式概念是“多項式時間可計算性”。大多數計算複雜性理論家都接受下述的假定:一個函數是可行的僅當它是多項式時間可計算的。
如前幾節所指出的,對概念的“形式刻畫”形成了邏輯、數學以及計算機科學的一個核心問題。對“形式刻畫”的合理性的驗證,隻能是非形式的。在計算機科學中還有著大量的“形式刻畫”作要做。
論形式化的局限性與“陷阱”
軟件技術的形式方法現在一般地被認為對計算機科學是重要的。但是.已使用形式方法多年的邏輯學家們的經驗指出,形式化作為一種方法,是有其局限性的,甚至存在著“陷阱”。所以,對邏輯與數學中形式化方法的曆史進行研究可能對於計算機科學是有幫助的.這一領域看起來是一種曆史性的研究,但它對於計算機科學中當前的研究是很有聯係的。
如所知,集合論的證明曆史中,宵經發現了“邏輯悖論”,這說明在形式化方法中存在著“陷阱並目.自從本世紀30年代以來,邏輯學家們已經認識到形式係統具有內在局限性,發現不完備的係統就說明了這一點。
卜麵,我們將給出幾個例來說明這種局限性和“陷阱”,並提出以卜的觀點~即:形式化巧法隻能通過經驗的方法來論證其正確性。
形式係統的完備性
1930年,數理邏輯學家在德國柯尼希堡舉行的數學家國際會議宣布下列的驚人結果,即:對任何給定的具有充分複雜性的形式係統,複雜到足以在其中表達所有的遞歸函數)而言,如果它是協調的,那麼這個係統是不完備的。這就是著名的完備性定理。
此外,上述定理有以下的推論:如果這樣一個係統是協調的,那麼它的協調性是不能在本係統內得到證明的。完備性定理和計算機科學是有關的。這一點是顯然的,因為全部遞歸函數在程序設計理論中都是可表示的,所以對於這一理論,如果它是協調的,那麼它是不完備的。計算機科學中的完備性的結果是由於形式化方法的局限性造成的。