2.1.1 命題演算
邏輯演算是數(shù)理邏輯的基礎(chǔ)，命題演算是邏輯演算最基本的組成部分。命題演算研究命題之間的關(guān)系，比如簡(jiǎn)單命題和復(fù)雜命題之間的關(guān)系，簡(jiǎn)單命題如何構(gòu)成復(fù)雜命題，由簡(jiǎn)單命題的真假如何推出復(fù)雜命題的真假等等。對(duì)于具體命題，我們不難通過(guò)機(jī)械運(yùn)算來(lái)達(dá)到我們的目的，這就是命題的算術(shù)。
、
對(duì)于命題演算最早是由美國(guó)邏輯學(xué)家波斯特在1921年給出證明的，他的證明方法是把命題化為標(biāo)準(zhǔn)形式—合取范式。教科書中常見(jiàn)的證明是匈牙利數(shù)學(xué)家卡爾馬給出的。除了這些構(gòu)造性證明之外，還有用布爾代數(shù)的非構(gòu)造性證明。
2.1.2 一階謂詞演算
在命題演算中，形式化的對(duì)象及演算的對(duì)象都是語(yǔ)句。但是，在數(shù)學(xué)乃至一般推理過(guò)程中，許多常見(jiàn)的邏輯推理并不能建立在命題演算的基礎(chǔ)上。例如：1．張三的每位朋友都是李四的朋友，王五不是李四的朋友，所以王五不是張三的朋友。因此，我們必須深入到語(yǔ)句的內(nèi)部，也就是要把語(yǔ)句分解為主語(yǔ)和謂語(yǔ)。
謂詞演算要比命題演算范圍寬廣得多，這由變?cè)部梢苑从吵鰜?lái)。命題演算的變?cè)皇钦Z(yǔ)句或命題，而謂詞演算的變?cè)腥悾簜�(gè)體變?cè)⒚}變?cè)�、謂詞變?cè)�。由于謂詞演算中有全稱量詞和存在量詞，在這些量詞后面的變化稱為約束變?cè)�，其他變�(cè)Q為自由變?cè)Ｗ詈?jiǎn)單的謂詞演算是狹義謂詞演算，現(xiàn)在通稱一階謂詞演算。
謂詞演算中的普遍有效公式與命題演算中的重言式還是有差別的。我們有行之有效的具體方法來(lái)判定一個(gè)公式是不是重言式。這種方法每一步都有明確的規(guī)定，并且可以在有限步內(nèi)完成，這種方法我們稱為能行的。但是在謂詞演算中，并沒(méi)有一種能行的方法來(lái)判定任何一個(gè)公式是否普遍有效的。這就需要尋找一種能行的方法來(lái)判定某個(gè)具體公式或一類公式是否普遍有效，這就是所謂判定問(wèn)題。它是數(shù)理邏輯中最主要的問(wèn)題之一。
一階謂詞演算的普遍有效公式也有一個(gè)公理系統(tǒng)。另外，同樣也有代入規(guī)則及推理規(guī)則。另外，還有約束變?cè)淖忠?guī)則等變形規(guī)則。在謂詞演算中也可以將每一個(gè)公式通過(guò)變形規(guī)則化為標(biāo)準(zhǔn)形式。其中最常用的是所謂前束范式，也就是公式中所有的量詞都放在最前面，而且還可以把前束范式進(jìn)一步化成斯科蘭路范式，它不但具有前束范式的形狀，而且每一個(gè)存在量詞都在所有全稱量詞之前。
利用范式可以解決許多問(wèn)題，最重要的是哥德?tīng)栕C明的一階謂詞演算的公理系統(tǒng)的完全性定理，即可以證明：公式A在公理系統(tǒng)中可以證明的當(dāng)且僅當(dāng)A是普遍有效的。同樣，一階謂詞演算的公理系統(tǒng)也是協(xié)調(diào)(無(wú)矛盾)的、相獨(dú)立的。1936年丘奇和圖林獨(dú)立的證明一階謂詞演算公式的一般判定問(wèn)題不可解問(wèn)題，可以變?yōu)槿ソ鉀Q具有特殊形式的范式公式的判定問(wèn)題。 |
