形式邏輯將論證的形式與其討論的主題分開。語法定義可接受的運算式與證明；語意則指派解釋與真值條件。將兩者關聯起來，便能精確陳述證明系統可以建立什麼，以及計算模型可以決定什麼。
語法與演繹 #
形式語言從符號字母表與良構公式的形成規則開始。命題邏輯包含命題變數與連接詞。一階邏輯加入變數、函式與述詞符號、常見形式中的等號，以及量詞。
演繹系統加入：
- 公理：不經推導即接受的公式，或能產生公式的公理模式；以及
- 推理規則：從前提推導結論的機械化模式。
推導是有限序列或樹，其中每個公式都是公理、假設，或推理規則的結果。符號 \(\Gamma \vdash \varphi\) 表示公式 \(\varphi\) 可由 \(\Gamma\) 中的假設推導。轉門符號描述語法：證明檢查器可以驗證推導，而不必決定其非邏輯符號的意義。
肯定前件律是一項推理規則：
P -> Q
P
------
Q形式系統在無法同時推導某公式與其否定時稱為一致。一致性不同於完備性，也不同於選定公理在預期模型中的真實性。
語意、模型與量化 #
命題邏輯的解釋會為每個原子命題指派 true 或 false。連接詞接著決定複合公式的真值：
| 公式 | 為真時 |
|---|---|
| \(P \land Q\) | 兩個運算元都為真 |
| \(P \lor Q\) | 至少一個運算元為真 |
| \(P \rightarrow Q\) | \(P\) 為假或 \(Q\) 為真 |
| \(P \leftrightarrow Q\) | 兩個運算元具有相同真值 |
一階語意需要非空域，以及對該域中每個常數、函式與述詞符號的解釋。變數指派為自由變數提供值。量詞在該域上取值：
- \(\forall x\, P(x)\) 在
P對每個域元素成立時為真； - \(\exists x\, P(x)\) 在
P至少對一個域元素成立時為真。
例如，\(\forall x (Human(x) \rightarrow Mortal(x))\) 不宣告存在任何人類。與 \(\exists x\, Human(x)\) 結合後，它蘊含 \(\exists x\, Mortal(x)\)。
一組公式的模型會使其中所有公式為真。符號 \(\Gamma \models \varphi\) 表示 \(\Gamma\) 的每個模型也是 \(\varphi\) 的模型。雙轉門符號描述語意後果，而不是推導的存在。
有效性、真實性、健全性與完備性 #
真實性屬於某個解釋下的公式。有效性則跨越解釋，屬於公式或論證：
- 當每個解釋都使公式為真時，公式在邏輯上有效。
- 當沒有解釋能使所有前提為真而結論為假時，論證有效。
- 健全論證有效，且其前提在預期解釋中為真。
因此，有效論證可以有假前提與假結論。有效性只保證真前提不能透過該論證形式導出假結論。
證明系統的性質將可推導性與語意後果連結起來：
soundness: if Gamma |- phi, then Gamma |= phi
completeness: if Gamma |= phi, then Gamma |- phi健全性表示規則不會推導無效的語意後果。完備性表示邏輯中可表達的每個語意後果都有推導。古典命題邏輯與一階邏輯都有健全且完備的證明系統。一階邏輯的 Gödel 完備性定理不可與其不完備定理混淆：具有足夠表達能力、一致且有效公理化的算術理論，不能證明其預期算術解釋中為真的每個陳述。
真值表可以決定命題有效性，因為具有有限變數的公式只有有限個賦值。一階有效性不能由相應的有限表決定，因為模型可以具有無界域。
圖靈機作為計算模型 #
確定性的單磁帶圖靈機可以由以下項目指定：
- 有限狀態集合，包括開始與停止狀態；
- 具有空白符號的有限磁帶字母表；
- 數學模型中無界的磁帶；
- 讀取並寫入單一儲存格的磁頭；以及
- 將目前狀態與掃描符號映射至新狀態、符號與磁頭移動的轉移函式。
組態記錄控制狀態、磁帶內容與磁頭位置。套用一次轉移函式會從一個組態移至下一個。當機器恰好接受某語言的字串時，它辨識該語言；當機器停止並對每個輸入回答時，它決定該語言。
可計算性與不可判定性 #
當圖靈機產生函式結果，並對函式域中的每個輸入停止時，函式即為圖靈可計算。包括 lambda 演算與暫存器機器在內的其他精確模型，計算相同類別的函式。Church-Turing 論題將該類別識別為有效可計算函式。該論題將數學模型連結至非形式概念，因此不是模型內部的定理。
可數多部機器描述演算法，但即使有限字母表上的語言也形成不可數集合。因此，有些語言無法由任何機器決定。停機問題提供建構性例子：沒有圖靈機能對每個編碼的機器與輸入決定該計算是否會停止。標準對角線論證假設存在這樣的判定器，建構一部在自身編碼上反駁判定器的機器，並拒絕該假設。
不可判定不代表每個實例都無法回答。靜態分析、定理證明器與型別系統仍然有用，因為它們限制語言、接受保守答案、要求註解，或在不決定每個語意性質的情況下終止。
評論
在 GitHub 上閱讀或評論（發表評論需要登入）