http://blog.163.com/lixiangdong2510@126/blog/static/349948212007059290124/
命題演算的形式系統被成功地構造出來了（前文我們將它表示為L），而且L是那么完美：系統內所能證明的公式“恰恰”是那些邏輯為真的公式，一個不多，一個不少。該系統恰如其分地抽象出命題演算的邏輯推理本質。
但是，邏輯學家們馬上發現L並非那么完美：L的功能太有限。於是，他們稍稍前進一步，將命題划分成更小的單位：主詞和謂詞。並試圖進而抽象出我們日常所進行的哪個事物具有哪個屬性的推理系統，從而揭示謂詞演繹的本質：這就是一階邏輯形式推理系統。
（主詞相當於主語，所討論的事物；謂詞相當於謂語，事物的屬性。主詞是變元或常元，謂詞是對相應變元屬性的判斷，可以對主詞使用量詞如所有、存在。但不去討論謂詞作為變元的情況，不對謂詞使用量詞。在高階邏輯中，可以對謂詞使用量詞。）
相似地，他們巧妙地構造了一個稍大的形式系統K，其中僅包含：
1 六條公理，這六條公理是推理的基礎；比形式系統L增加了3條關於量詞的公理。
2 兩條規則，據此規則進行推理；比形式系統L增加了1條規則，也是關於量詞的。
並且證明了：
3 K演繹出的公式都是“邏輯為真的”（K的可靠性Soundness）；
4 任何“邏輯為真”的公式都可以由K推理出來（K的完備性Completeness）.
這就是形式化的謂詞演算系統（一階邏輯形式系統）。
這似乎是顯而易見的。但事實上，這一結論最早的證明直到1930年才由哥德爾（Godel）提出來。從1910 年羅素（B.Russell）在《數學原理》中提出的第一個完全形式化的一階謂詞邏輯系統PM算起，用了20年，如果從亞里士多德公元前300年提出謂詞演算的思想，到哲學家、邏輯學家們得到這個結果，2200多年已經過去了。
在命題演算系統中，一個公式（結論）是由命題作為最小單位，加上聯結詞聯結而成。公式非真即假，其值由命題單位的賦值決定，即一個公式對應一個真值表。所謂“邏輯為真”就是“重言式”，即真值表中公式的取值總是“真”。
與命題演算系統不同，謂詞演算系統要復雜的多。首先是不能使用真值表來判斷公式的邏輯真假。其實如果沒有相應的解釋，一個不含量詞的公式連真假的意義都談不上。如F(x)表示x會飛，如果不說明x是什么，則F(x)沒有真假可言。所以論證一階邏輯中3、4兩個性質，就要涉及到解釋、賦值、滿足、模型等概念。