2.1.1 命題演算

邏輯演算是數(shù)理邏輯的基礎(chǔ)，命題演算是邏輯演算最基本的組成部分。命題演算研究命題之間的關(guān)系，比如簡單命題和復(fù)雜命題之間的關(guān)系，簡單命題如何構(gòu)成復(fù)雜命題，由簡單命題的真假如何推出復(fù)雜命題的真假等等。對于具體命題，我們不難通過機(jī)械運(yùn)算來達(dá)到我們的目的，這就是命題的算術(shù)。 、

對于命題演算最早是由美國邏輯學(xué)家波斯特在1921年給出證明的，他的證明方法是把命題化為標(biāo)準(zhǔn)形式—合取范式。教科書中常見的證明是匈牙利數(shù)學(xué)家卡爾馬給出的。除了這些構(gòu)造性證明之外，還有用布爾代數(shù)的非構(gòu)造性證明。

2.1.2 一階謂詞演算

在命題演算中，形式化的對象及演算的對象都是語句。但是，在數(shù)學(xué)乃至一般推理過程中，許多常見的邏輯推理并不能建立在命題演算的基礎(chǔ)上。例如：1．張三的每位朋友都是李四的朋友，王五不是李四的朋友，所以王五不是張三的朋友。因此，我們必須深入到語句的內(nèi)部，也就是要把語句分解為主語和謂語。

謂詞演算要比命題演算范圍寬廣得多，這由變元也可以反映出來。命題演算的變元只是語句或命題，而謂詞演算的變元有三類：個體變元、命題變元、謂詞變元。由于謂詞演算中有全稱量詞和存在量詞，在這些量詞后面的變化稱為約束變元，其他變元稱為自由變元。最簡單的謂詞演算是狹義謂詞演算，現(xiàn)在通稱一階謂詞演算。

謂詞演算中的普遍有效公式與命題演算中的重言式還是有差別的。我們有行之有效的具體方法來判定一個公式是不是重言式。這種方法每一步都有明確的規(guī)定，并且可以在有限步內(nèi)完成，這種方法我們稱為能行的。但是在謂詞演算中，并沒有一種能行的方法來判定任何一個公式是否普遍有效的。這就需要尋找一種能行的方法來判定某個具體公式或一類公式是否普遍有效，這就是所謂判定問題。它是數(shù)理邏輯中最主要的問題之一。

一階謂詞演算的普遍有效公式也有一個公理系統(tǒng)。另外，同樣也有代入規(guī)則及推理規(guī)則。另外，還有約束變元改字規(guī)則等變形規(guī)則。在謂詞演算中也可以將每一個公式通過變形規(guī)則化為標(biāo)準(zhǔn)形式。其中最常用的是所謂前束范式，也就是公式中所有的量詞都放在最前面，而且還可以把前束范式進(jìn)一步化成斯科蘭路范式，它不但具有前束范式的形狀，而且每一個存在量詞都在所有全稱量詞之前。

利用范式可以解決許多問題，最重要的是哥德爾證明的一階謂詞演算的公理系統(tǒng)的完全性定理，即可以證明：公式A在公理系統(tǒng)中可以證明的當(dāng)且僅當(dāng)A是普遍有效的。同樣，一階謂詞演算的公理系統(tǒng)也是協(xié)調(diào)(無矛盾)的、相獨(dú)立的。1936年丘奇和圖林獨(dú)立的證明一階謂詞演算公式的一般判定問題不可解問題，可以變?yōu)槿ソ鉀Q具有特殊形式的范式公式的判定問題。