推導

在有效性中，我們引入了公式和論證的有效性概念。在命題邏輯中，有效公式是重言式。到目前為止，我們可以用以下方法證明公式 $\varphi \,\!$ 是有效的（重言式）。

為 $\varphi \,\!$ 製作真值表。

獲得 $\varphi \,\!$ 作為已知有效的公式的代入例項。

透過將等價替換應用於已知有效的公式，獲得 $\varphi \,\!$ 。

然而，這些方法在謂詞邏輯中失效，因為謂詞沒有真值表。如果沒有替代方法，我們就無法使用第二種和第三種方法，因為它們依賴於對其他公式有效性的瞭解。另一種證明公式有效的方法——不使用真值表——是使用推導。本頁和後續頁面介紹了這種技術。請注意，推導證明論證有效的斷言假設了一個健全的推導系統，參見下面的健全性。

推導是一系列編號行，每行都包含一個公式和一個註釋。註釋提供了將該行新增到推導的理由。推導是數學證明的高度形式化的類比——或者說是數學證明的模型。

一個典型的推導系統將允許以下幾種型別的行

一行可以是公理。推導系統可以指定一組公式作為公理。這些公理在任何推導中都被認為是正確的。對於命題邏輯，公理集是重言式的固定子集。

一行可以是假設。推導可以有幾種型別的假設。以下列出了標準情況。

前提。當試圖證明一個論證的有效性時，可以假設該論證的前提。

用於子推導的臨時假設。此類假設旨在僅在推導的一部分中有效，並且必須在推導完成之前被解除（使其失效）。子推導將在後面的頁面中介紹。

一行可以是將推理規則應用於前幾行得出的結果。推理是指對前幾行進行的句法轉換以生成新行。推理必須遵循推導系統定義的固定模式集之一。這些模式是系統的推理規則。其思想是，任何符合推理規則的推理都應該是有效的論證。

健全性和有效性

我們在形式語義學中注意到，像 ${\mathcal {L_{S}}}\,\!$ 這樣的形式語言可以通過幾種替代甚至相互競爭的語義規則集來解釋。對於給定的語法語義對，還可以定義多種推導系統。由形式語法、形式語義和推導系統組成的三元組是一個邏輯系統。

推導旨在證明論證是有效的。零前提論證的推導旨在證明其結論是一個有效公式——在命題邏輯中，這意味著證明它是重言式。給定一個邏輯系統，如果推導系統實現了這些目標，則稱該系統是健全的。也就是說，一個推導系統是健全的（具有健全性的屬性），如果它的推導系統中可推導的每個公式（和論證）都是有效的（給定一個語法和一個語義）。

推導系統的另一個理想品質是完備性。給定一個邏輯系統，如果它的推導系統可以推匯出每個有效公式，則稱該系統是完備的。然而，對於某些邏輯，沒有推導系統是或可以是完備的。

健全性和完備性是重要的結果。它們的證明在這裡不作介紹，但在許多標準的元邏輯教科書中都有介紹。

推導符號

$\vDash \,\!$ 符號有時被稱為推導符號，特別是語義推導符號。我們之前介紹了該符號的以下三種用法。

(1)	${\mathfrak {v}}\vDash \varphi \,\!$	${\mathfrak {v}}\,\!$ 滿足 $\varphi \,\!$ 。
(2)	$\vDash \varphi \,\!$	$\varphi \,\!$ 是有效的。
(3)	$\Gamma \vDash \varphi \,\!$	$\Gamma \,\!$ 蘊含（具有邏輯結果） $\varphi \,\!$ 。