一阶逻辑 是使用於数学 、哲学 、语言学 及電腦科學 中的一种形式系统 ,也可以稱為:一阶斷言演算 、低階斷言演算 、量化理論 或谓词逻辑 。一階邏輯和命題邏輯 的不同之處在於,一階邏輯包含量詞 。
高階邏輯 和一階邏輯不同之處在於,高階邏輯的斷言符號可以有斷言符號或函數符號當做引數 ,且容許斷言量詞或函數量詞[ 1] 。在一階邏輯的語義 中,斷言被解釋為關係 。而高階邏輯的語義裡,斷言則會被解釋為集合的集合。
在通常的語義下,一階邏輯是可靠 (所有可證的敘述皆為真)且完備 (所有為真的敘述皆可證)的。雖然一階邏輯的邏輯歸結只是半可判定性 的,但還是有許多用於一階邏輯上的自動定理證明 。一階邏輯也符合一些使其能通過證明論 分析的元邏輯 定理,如勒文海姆–斯科倫定理 及緊緻性定理 。
一階邏輯是數學基礎 中很重要的一部份。許多常見的公理系統,如一階皮亞諾公理 、冯诺伊曼-博内斯-哥德尔集合论 和策梅洛-弗蘭克爾集合論 都是一階理論。然而一階邏輯不能控制其無窮模型的基數 大小,因根據勒文海姆–斯科倫定理和康托爾定理 ,可以構造出一種“病態”集合論模型,使整個模型可數,但模型內卻會覺得自己有「不可數集」。類似地,可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論 。但一階的直覺主義邏輯 裡,勒文海姆–斯科倫定理不可證明[ 2] ,故不會有以上之現象。
命題邏輯顧名思義,會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假 的敘述簡記為 p {\displaystyle p} 及 q {\displaystyle q} (也就是有真有假的命題 ),然後討論 ¬ p {\displaystyle \neg p} (非p)、 p ⇒ q {\displaystyle p\Rightarrow q} (若p則q)、 p ∧ q {\displaystyle p\wedge q} (p且q)與 p ∨ q {\displaystyle p\vee q} (p或q)之間的推理關係。
但一階邏輯嘗試從一些比較基礎的詞彙去建構「句子」,比如說,可用符號 Phil ( x ) {\displaystyle {\text{Phil}}(x)} 代表 「 x 是哲學家」,也就是賦予斷言符號 「 Phil ( x ) {\displaystyle {\text{Phil}}(x)} 」語意的解釋。 這個解釋預設一個「所有人類的群體」(也就是下面標準語義 一節會說到的论域 ),并將變數 x {\displaystyle x} 對應為自群體中取出來的某人。
以此類推,斷言符號可以包含一個以上的變數。例如:可以將 Cp ( x , y ) {\displaystyle {\text{Cp}}(x,\,y)} 解釋為「 x 與 y 是夫妻」。
一階邏輯類似於命題邏輯,可以將斷言符號與 ¬ {\displaystyle \neg } (非)、 ⇒ {\displaystyle \Rightarrow } (則)、 ∧ {\displaystyle \wedge } (且)和 ∨ {\displaystyle \vee } (或)組成更複雜的敘述,例如:把斷言符號 Schol ( x ) {\displaystyle {\text{Schol}}(x)} 解釋成「 x {\displaystyle x} 是學者」,那「若 x 為哲學家,則 x 為學者」可表示為:
Phil ( x ) ⇒ Schol ( x ) {\displaystyle {\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)\,} 但相較之下,一階邏輯又加入了描述「所有」與「存在」的量詞,比如說「對所有 x ,若 x 為哲學家,則 x 為學者」可記為:
∀ x [ Phil ( x ) ⇒ Schol ( x ) ] {\displaystyle \forall x[{\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)]} 也就是自左方開始閱讀,將 ∀ x {\displaystyle \forall x} 解釋成「对所有 x 有…」。 ∀ {\displaystyle \forall } 這個符號被称为全稱量詞 。
而對於「有 x 是哲學家」这一叙述,一階邏輯則引入另一種量詞:
∃ x [ Phil ( x ) ] {\displaystyle \exists x[{\text{Phil}}(x)]} 也就是自左方開始閱讀,將 ∃ x {\displaystyle \exists x} 解釋成「存在 x {\displaystyle x} 使…」。 ∃ {\displaystyle \exists } 這個符號被称为存在量詞 。
順帶一提「並非所有 x 不是哲學家」等價於「有 x 是哲學家」;且「不存在 x 不是學者」也等價於「所有的 x 是學者」。所以可以用「否定」和「全稱量詞」來組合出「存在量詞」。換句話說,可作以下的符號定義( A {\displaystyle {\mathcal {A}}} 代表一段「敘述」):
∃ x A := ¬ [ ∀ x ( ¬ A ) ] {\displaystyle \exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]} 一階邏輯也考慮到「相等」這個概念在敘述中的重要性,例如想表達「若所有 x {\displaystyle x} 是哲學家,那 x {\displaystyle x} 的長子也會是哲學家」,可先把 Son ( x ) {\displaystyle {\text{Son}}(x)} 解釋為 「 x 的長子」,那么這段敘述可記為:
∀ x Phil ( x ) ⇒ Phil [ Son ( x ) ] {\displaystyle \forall x{\text{Phil}}(x)\Rightarrow {\text{Phil}}[{\text{Son}}(x)]} 換句話說, Son ( x ) {\displaystyle {\text{Son}}(x)} 被解釋成「與 x {\displaystyle x} 有特定且唯一對應關係」的某對象(被稱為函數符號 )。換句話話說,只要「 x {\displaystyle x} 就是 y {\displaystyle y} 」,那「 x {\displaystyle x} 的長子也會是 y {\displaystyle y} 的長子」。換句話說:
( x = y ) ⇒ [ Son ( x ) = Son ( y ) ] {\displaystyle (x=y)\Rightarrow [{\text{Son}}(x)={\text{Son}}(y)]} 這些性質被一階邏輯視為「理所當然」。
類似地,敘述中也有一些「不變的實體」,如苏格拉底 ,表示這些「實體」的符號被稱為常數符號。例如將 s {\displaystyle s} 解釋為苏格拉底 ,那「苏格拉底 為哲學家」就可以寫成:
Phil ( s ) {\displaystyle {\text{Phil}}(s)} 所謂的「不變」隱含的代表:
「蘇格拉底就是蘇格拉底」 「對所有x,對所有y,如果x就是蘇格拉底,且y就是蘇格拉底,那x就是y」 換句話說
( s = s ) {\displaystyle (s=s)} ∀ x ∀ y { [ ( x = s ) ∧ ( y = s ) ] ⇒ ( x = y ) } {\displaystyle \forall x\forall y\{[(x=s)\wedge (y=s)]\Rightarrow (x=y)\}} 這兩個性質也被一階邏輯視為「理所當然」。
一階邏輯的形式理論 可分成幾個部份:
語法 :決定哪些符號組合是合式公式 。(直觀上的“文法無誤的敘述”) 推理規則:由合式公式符號組合出新合式公式的規則(直觀上的“推理”) 公理:一套合式公式(直觀上的基本假設) 一套理論能容許多少符號,取決於人類能運用物理定律 來塑造多少符號,但目前無法確知宇宙是不是有限,或是以可無限制地分割。雖然所有的公理化集合論 都以量詞的形式隱晦的承認跟自然數 一樣多的無窮(如ZF集合論的無窮公理 ),甚至以這樣的可數無窮為基礎,去建構出不可數 的實數,但將抽象的理論對應到現實時,還是需要回答物理上有沒有可數或不可數的無窮。所以謹慎起見,如果沒有特別申明的話,以下各種類符號的數目上限都是有限的。
一階邏輯通常擁有以下的符號:
量化符號 ∀ {\displaystyle \forall } 及 ∃ {\displaystyle \exists } 某些作者[ 3] 會把 ∃ {\displaystyle \exists } 符號定義為 ∃ x A := ¬ [ ∀ x ( ¬ A ) ] {\displaystyle \exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]} ,如此便只需要 ∀ {\displaystyle \forall } 做為基礎符號。 邏輯聯結詞 :以下為可能的表示符號(关于波蘭表示法下的邏輯連接詞,請參見逻辑运算的波兰记法 ): 否定 : ¬ {\displaystyle \neg } 或 ∼ {\displaystyle \sim } 或- 條件 : ⇒ {\displaystyle \Rightarrow } 或 → {\displaystyle \rightarrow } 或 ⊃ {\displaystyle \supset } 且 : ∧ {\displaystyle \land } 或 & {\displaystyle \&} 或 : ∨ {\displaystyle \lor } 或 || 雙條件 : ⇔ {\displaystyle \Leftrightarrow } 或 ↔ {\displaystyle \leftrightarrow } 某些作者[ 4] 會作如下的符號定義: A ∧ B := ¬ ( A ⇒ ( ¬ B ) ) , {\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}:=\neg ({\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})),} A ∨ B := ( ¬ A ) ⇒ B , {\displaystyle {\mathcal {A}}\vee {\mathcal {B}}:=(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}},} A ⇔ B := ( A ⇒ B ) ∧ ( B ⇒ A ) , {\displaystyle {\mathcal {A}}\Leftrightarrow {\mathcal {B}}:=({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}}),} 如此一來只需要否定 和條件 做為基礎符號。 標點符號:括號、逗號及其他,依作者的喜好有所不同。 為了更有效的將括號做配對,通常還會採用大括號{ } 跟中括號[ ] 。 至多跟自然數 一樣多的變數 ,通常標記為英文字母末端的小寫字母x 、y 、z 、…,也常會使用下標(或上標、上下標兼有)來區別不同的變數:x 0 、x 1 、x 2 、…(特別注意c有時候會被當成常數符號而引起混淆)。 等式符號: = {\displaystyle =} 有作者會因為語義上对“相等”的不同解释,而將等式符號視為雙元斷言符號、甚至是某種合式公式 的簡寫。 符號相等: ≍ {\displaystyle \asymp } 某些作者[ 5] 會額外採用這個符號來表示符號辨識上的等同 以便與等式符號作區別。 並非所有的符號都不可或缺的,像謝費爾豎線 「 | {\displaystyle |} 」(或異或 )可以用來定義量詞以外的所有邏輯符號,換句話說:
符號定義 — ( ¬ A ) := ( A | A ) {\displaystyle (\neg {\mathcal {A}}):=({\mathcal {A}}|{\mathcal {A}})}
( A ⇒ B ) := A | ( B | B ) {\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}}):={\mathcal {A}}|({\mathcal {B}}|{\mathcal {B}})}
( A ∧ B ) := [ ( A | B ) | ( A | B ) ] {\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {B}})|({\mathcal {A}}|{\mathcal {B}})\,]}
( A ∨ B ) := [ ( A | A ) | ( B | B ) ] {\displaystyle ({\mathcal {A}}\vee {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {A}})|({\mathcal {B}}|{\mathcal {B}})\,]}
另外,一些作者不區分語義解釋 和形式理論 ,所以會將表示真值的符號納入形式理論裡,也就是說,用 T 、Vpq 或 ⊤ {\displaystyle \top } 來表示「真」,並用 F 、 Opq 或 ⊥ {\displaystyle \bot } 來表示「假」。
「他們兩人是夫妻」,是一個關於兩個“對象”的斷言,而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數 n {\displaystyle n} 、 j {\displaystyle j} 約定:
A j n ( x 1 , x 2 , . . . , x n ) {\displaystyle A_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})} 為一階邏輯的合法詞彙。它在直觀上表示一個有 n {\displaystyle n} 個“對象”的斷言,稱為 n {\displaystyle n} 元斷言符號 。下標的自然數 j {\displaystyle j} 只是拿來和其他同為 n {\displaystyle n} 元的斷言符號作區別。
實用上只要有申明,不至於和其他詞彙引起混淆的話,可以用任意的形式簡寫一個斷言符號。如:公理化集合論 裡的雙元斷言符號 A 1 2 ( x , y ) {\displaystyle A_{1}^{2}(x,\,y)} 也可以表示为 x ∈ y {\displaystyle x\in y} 。
「物體的顏色」、「夫妻的長子」这种断言說明了一组對象所唯一 對應的對象。但不同的夫妻有不同的長子;不同的物體有不同的顏色。據此,形式上對於自然數 n {\displaystyle n} 、 j {\displaystyle j} 約定:
f j n ( x 1 , x 2 , . . . , x n ) {\displaystyle f_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})} 為一階邏輯的合法詞彙,直觀上表示 n {\displaystyle n} 個“對象”所對應到的東西,稱它為 n {\displaystyle n} 元函數符號 。需要特別注意 ,這種“唯一對應”的直觀想法,必須配上關於“等式”的性質(詳見下面的等式定理 章节),才能在形式理論中被實現。
与斷言符號一样,只要不引起混淆,就可以用任何的形式簡寫函數符號。如:公理化集合論 裡的 x ∪ y {\displaystyle x\cup y} 是依據聯集公理 而定義的新函數符號(請參見下面函數符號與唯一性 章節),也可以冗長的表記為 f j 2 ( x , y ) {\displaystyle f_{j}^{2}(x,\,y)} 。
「刻度0」、「原點」、「蘇格拉底 」是直觀上"唯一不變"的對象。據此,對自然數 j {\displaystyle j} 約定
c j {\displaystyle c_{j}} 為一階邏輯的合法詞彙,直觀上表示一個“唯一不變”的對象,稱為常數符號 。同樣的。“常數的不變性”需配上等式的性質(詳見下面等式定理 )才能被實現。
為了不和變數的表記混淆,常數符號一樣可以用任何的形式簡寫,如公理化集合論 裡的 ∅ {\displaystyle \varnothing } 是根據空集公理 和函數符號與唯一性 ,而定義的新常數符號。亦可冗長的表示為 c j {\displaystyle c_{j}} 。
和自然語言(如英語 )不同,一階邏輯的語言以明確的遞迴 定義判斷一個給定的詞彙是否合法。大致上來說,一階邏輯以「項」代表討論的對象,而對「項」的斷言組成了最基本的原子(合式)公式 ;而原子公式和邏輯符號組成了更複雜的合式公式 (也就是“敘述”)。
「那對夫妻的長子的職業」、「 ( x + y ) × z {\displaystyle (x+y)\times z} 」、「 x ∪ ∅ {\displaystyle x\cup \varnothing } 」代表變數可以與函數符號組成更一般的物件。據此形式,遞迴地規定一類合法詞彙——項 為:
遞迴定義 —
變數 和常數 是項。 若 T 1 , . . . . , T n {\displaystyle T_{1},\,....,\,T_{n}} 全都是項,那么 f j n ( T 1 , . . . . , T n ) {\displaystyle f_{j}^{n}(T_{1},\,....,\,T_{n})} 也是項。 項只能通过以上兩點,於有限步驟內建構出來。 習慣上以大寫的西方字母(如英文 字母、希伯來 字母、希臘字母 )代表項,如果變數不得不採用大寫字母,而可能跟項引起混淆的話,需額外規定分辨的辦法。
為了比較簡潔地規定甚麼是合式公式 ,先規定原子公式 為:(若 T 1 , . . . . , T n {\displaystyle T_{1},\,....,\,T_{n}} 是項)
A j n ( T 1 , . . . . , T n ) {\displaystyle A_{j}^{n}(T_{1},\,....,\,T_{n})} 這樣的形式。
一階邏輯的合式公式 (簡稱公式或 w f {\displaystyle wf} )以下面的規則遞迴地定義:
另外成對的中括弧跟大括弧,符號辨識上視為成對的小括弧,而草書的大寫西方字母 為公式的代號。
舉例來說,
{ ( ∀ y ) A 1 2 [ x , f 1 1 ( y ) ] } {\displaystyle \{(\forall y)A_{1}^{2}[x,\,f_{1}^{1}(y)]\}} 是公式而
∀ x x ⇒ {\displaystyle \forall x\,x\Rightarrow } 則不是公式。
而接下來只要對任意公式 A {\displaystyle {\mathcal {A}}} 、 B {\displaystyle {\mathcal {B}}} 與變數 x {\displaystyle x} ,做以下符號定義
符號定義 — ( A ∧ B ) := { ¬ [ A ⇒ ( ¬ B ) ] } {\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}}):=\{\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]\}}
( A ∨ B ) := [ ( ¬ A ) ⇒ B ] {\displaystyle ({\mathcal {A}}\vee {\mathcal {B}}):=[(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
( A ⇔ B ) := [ ( A ⇒ B ) ∧ ( B ⇒ A ) ] {\displaystyle ({\mathcal {A}}\Leftrightarrow {\mathcal {B}}):=[({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}})]}
( ∃ x A ) := { ¬ [ ∀ x ( ¬ A ) ] } {\displaystyle (\exists x{\mathcal {A}}):=\{\neg [\forall x(\neg {\mathcal {A}})]\}} (同樣美觀起見 ( ∃ x ) A := ∃ x A {\displaystyle (\exists x){\mathcal {A}}:=\exists x{\mathcal {A}}} )
這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。
所謂的施用 /作用 ,是以下公式形式的口語說法:(其中 A {\displaystyle {\mathcal {A}}} 與 B {\displaystyle {\mathcal {B}}} 都是公式)
( ¬ A ) {\displaystyle (\neg {\mathcal {A}})} 稱為 ¬ {\displaystyle \neg } 施用於 A {\displaystyle {\mathcal {A}}} 上。 ( A ⇒ B ) {\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})} 稱為 ⇒ {\displaystyle \Rightarrow } 施用於 A {\displaystyle {\mathcal {A}}} 和 B {\displaystyle {\mathcal {B}}} 上。 ( A ∧ B ) {\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})} 稱為 ∧ {\displaystyle \wedge } 施用於 A {\displaystyle {\mathcal {A}}} 和 B {\displaystyle {\mathcal {B}}} 上。 ( A ∨ B ) {\displaystyle ({\mathcal {A}}\vee {\mathcal {B}})} 稱為 ∨ {\displaystyle \vee } 施用於 A {\displaystyle {\mathcal {A}}} 和 B {\displaystyle {\mathcal {B}}} 上。 ( A ⇔ B ) {\displaystyle ({\mathcal {A}}\Leftrightarrow {\mathcal {B}})} 稱為 ⇔ {\displaystyle \Leftrightarrow } 施用於 A {\displaystyle {\mathcal {A}}} 和 B {\displaystyle {\mathcal {B}}} 上。 ( ∀ x A ) {\displaystyle (\forall x{\mathcal {A}})} 稱為 ∀ x {\displaystyle \forall x} 施用於 A {\displaystyle {\mathcal {A}}} 上。 ( ∃ x A ) {\displaystyle (\exists x{\mathcal {A}})} 稱為 ∃ x {\displaystyle \exists x} 施用於 A {\displaystyle {\mathcal {A}}} 上。 就类似于運算子作用在它們身上。
量詞所施用的公式被稱為量詞的範圍 (scope)。同一個變數在公式一般來說不只出現一次,若變數 x {\displaystyle x} 出現在 ∀ x {\displaystyle \forall x} 的範圍內,稱這樣出現的 x {\displaystyle x} 為不自由 /被約束的 x {\displaystyle x} (not free/bounded);反過來說,不出現在 ∀ x {\displaystyle \forall x} 的範圍內的某個 x {\displaystyle x} 被稱為自由的 x {\displaystyle x} 。
例如,對於公式:
{ ( ∀ x ) [ A 1 1 ( x ) ⇒ A 2 1 ( y ) ] } {\displaystyle \{(\forall x)[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]\}} [ A 1 1 ( x ) ⇒ A 2 1 ( y ) ] {\displaystyle [A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]} 就是量詞 ∀ x {\displaystyle \forall x} 的範圍;而 A 1 1 ( x ) {\displaystyle A_{1}^{1}(x)} 裡的 x {\displaystyle x} 就是不自由的;反之 A 2 1 ( y ) {\displaystyle A_{2}^{1}(y)} 裡的 y {\displaystyle y} 就是自由的。
說 x {\displaystyle x} 於公式 A {\displaystyle {\mathcal {A}}} 完全自由,意為於 A {\displaystyle {\mathcal {A}}} 出現的 x {\displaystyle x} 都是自由的;反之,說 x {\displaystyle x} 於公式 A {\displaystyle {\mathcal {A}}} 完全不自由/完全被約束,意為 A {\displaystyle {\mathcal {A}}} 內根本沒有 x {\displaystyle x} ,或是 A {\displaystyle {\mathcal {A}}} 內沒有自由的 x {\displaystyle x} 。若 A {\displaystyle {\mathcal {A}}} 內所有的變數都完全不自由, A {\displaystyle {\mathcal {A}}} 特稱為封閉公式/句子 (closed formula/sentence)。
括弧是為了保證語意解釋符合預期,但太多的括弧書寫不易,為此規定以下的“重構法”(反過來就是“簡寫法”),從表面上不合法的一串符號找出作者原來想表達的公式:
若整串符號的括弧不成對,直接視為無法重構 。 以 ¬ , ∧ , ∨ , ∀ , ∃ , ⇒ , ⇔ {\displaystyle \lnot ,\,\land ,\,\lor ,\,\forall ,\,\exists ,\,\Rightarrow ,\,\Leftrightarrow } (左至右)的施用順序重構括弧。 相鄰的邏輯連接詞或量詞無法決定施用順序的話,以右邊為先。 重構施用的順序,以被成對括弧包住的部分為優先施用,其次才是落單的斷言符號。 舉例來說
¬ [ ∀ x A 1 1 ( x ) ] ⇒ ∃ x ¬ A 2 1 ( x ) {\displaystyle \lnot [\forall xA_{1}^{1}(x)]\Rightarrow \exists x\lnot A_{2}^{1}(x)} 的重構過程如下
{ ¬ [ ∀ x A 1 1 ( x ) ] } ⇒ ∃ x [ ¬ A 2 1 ( x ) ] {\displaystyle \{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)]} (優先施用 ¬ {\displaystyle \lnot } ) { ¬ [ ∀ x A 1 1 ( x ) ] } ⇒ { ∃ x [ ¬ A 2 1 ( x ) ] } {\displaystyle \{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}} (施用 ∃ {\displaystyle \exists } ) { { ¬ [ ∀ x A 1 1 ( x ) ] } ⇒ { ∃ x [ ¬ A 2 1 ( x ) ] } } {\displaystyle \{\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}\}} (最後施用 ⇒ {\displaystyle \Rightarrow } ) 可以被重構為公式的一串符號則寬鬆的認定為“合式公式”。(最明顯的例子就是合式公式最外層的括弧可以省略)
波蘭表示法 將邏輯連接詞前置於被施用的公式 而非傳統的中間。如果沿用以上的"施用順序",這個表示法允許捨棄所有括弧。如公式
∀ x ∀ y { A 1 1 [ f 1 1 ( x ) ] ⇒ ¬ { A 1 1 ( x ) ⇒ A 1 3 [ f 1 1 ( y ) , x , z ] } } {\displaystyle \forall x\forall y\{A_{1}^{1}[f_{1}^{1}(x)]\Rightarrow \neg \{A_{1}^{1}(x)\Rightarrow A_{1}^{3}[f_{1}^{1}(y),x,z]\}\}} 轉成波蘭表示法的過程如下
∀ x ∀ y ⇒ A 1 1 f 1 1 x ¬ ⇒ A 1 1 x A 1 3 f 1 1 y x z {\displaystyle \forall x\forall y\Rightarrow A_{1}^{1}f_{1}^{1}x\neg \Rightarrow A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz} (轉成波蘭表示法的順序) Π x Π y C A 1 1 f 1 1 x N C A 1 1 x A 1 3 f 1 1 y x z {\displaystyle \Pi x\Pi y{\text{C}}A_{1}^{1}f_{1}^{1}x{\text{N}}{\text{C}}A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz} (邏輯連結詞的符號轉換) 一階邏輯通常只有以下的推理規則(因為將普遍化 視為推理規則會有不直觀的限制)
直觀意義非常明顯,就是p =>q 且p 可以推出q 。
在只以謝費爾豎線 「 | {\displaystyle |} 」為基礎邏輯連接詞的公理系统 裡,MP律 會被改寫成
它们实际上是公理模式 ,代表著“跟自然數一樣多”條的公理。
在有(A1)與(A2)的前提下,(A3)等價於以下的公理模式:(證明請參見下面否定 一節。)
(T1) — [ ( ¬ B ) ⇒ ( ¬ C ) ] ⇒ ( B ⇒ C ) {\displaystyle [\,(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})\,]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})}
另外,在只以謝費爾豎線 「 | {\displaystyle |} 」為基礎邏輯連接詞的公理系统 裡,上面三條公理模式等價於下面這條公理模式[ 3] :
公理 — 如果 B {\displaystyle {\mathcal {B}}} 、 C {\displaystyle {\mathcal {C}}} 、 D {\displaystyle {\mathcal {D}}} 、 E {\displaystyle {\mathcal {E}}} 和 F {\displaystyle {\mathcal {F}}} 都是公式,則:
[ B | ( C | D ) ] | { [ E | ( E | E ) ] | { ( F | C ) | [ ( B | F ) | ( B | F ) ] } } {\displaystyle [\,{\mathcal {B}}|({\mathcal {C}}|{\mathcal {D}})\,]|{\big \{}\,[\,{\mathcal {E}}|({\mathcal {E}}|{\mathcal {E}})\,]|\{\,({\mathcal {F}}|{\mathcal {C}})|[\,({\mathcal {B}}|{\mathcal {F}})|({\mathcal {B}}|{\mathcal {F}})\,]\,\}\,{\big \}}} 都是公理。
它们实际上也是公理模式 。
根據不同作者的看法,甚至是理論本身的需求,「等式」在形式理論裡可能是斷言符號或是一段公式(如 a 等於 b 可定義為對所有的 x , x 屬於 a 等價於 x 屬於 b )。而如何刻劃直觀上「等式的性質」,有一開始就將「等式的性質」視為公理(模式),但也有視為元定理 的另一套處理方法,以下暫且以公理模式 的方式處理。以元定理處理的方法會在等式定理 詳述。
事實上這兩個公理模式也確保了函數符號“唯一對應”和常數符號的“唯一性”,但證明這些性質需要一些元定理 ,簡便起見合併於下面的等式定理 一節講述。
一階邏輯的標準語義 源於波蘭邏輯學家阿尔弗雷德·塔斯基 所著《On the Concept of Truth in Formal Languages》 。根據上面語法 一節,公式是由原子公式遞迴地添加邏輯連結詞而來的,而原子公式是由斷言符號與項所構成的。所以要檢驗一條公式在特定的論域下正不正確,就要規定項的取值 ,然後檢驗這樣的取值會不會落在斷言符號所對應的關係 裡。由此延伸出所有公式的“真假值“。
也就是一套一階邏輯的語義解釋,要包含
變數取值的論域 如何解釋函數符號(為論域中的某個函數)與常數符號(為論域中的某特定元素),以便從特定的變數取值得出項的取值。 如何將斷言符號與論域裡的某關係做對應。 通常一套解釋方法(簡稱為解釋 )會以代號 M {\displaystyle M} 表示。
量詞的解釋 需要指明變數取值範圍的論域 ——也就是一個集合 D {\displaystyle D} 。而變數可能跟自然數一樣多,換句話說,所有變數在論域 D {\displaystyle D} 取的值可以依序以自然數標下標——也就是一個在 D {\displaystyle D} 取值的數列 。如果以 x 1 , x 2 , x 3 , ⋯ {\displaystyle x_{1},\,x_{2},\,x_{3},\,\cdots } 的代號(不一定是變數本身的表示符號)來列舉變數,那麼從 D {\displaystyle D} 的某套變數取值就以
⟨ a k ⟩ k ∈ N {\displaystyle \left\langle a_{k}\right\rangle _{k\in \mathbb {N} }} 或較直觀的符號
⟨ a 1 , a 2 , a 3 , ⋯ ⟩ {\displaystyle \left\langle a_{1},\,a_{2},\,a_{3},\,\cdots \right\rangle } 來表示。
一套解釋 M {\displaystyle M} 會將 n {\displaystyle n} 元函數符號 f i n {\displaystyle f_{i}^{n}} 解釋成某個 ( f i n ) M : D n → D {\displaystyle {(f_{i}^{n})}^{M}:D^{n}\to D} 的 n {\displaystyle n} 元函數 ;而常數符號 c l {\displaystyle c_{l}} 解釋成特定的 c l M ∈ D {\displaystyle {c_{l}}^{M}\in D} (亦稱為 c l {\displaystyle c_{l}} 的取值為 c l M {\displaystyle {c_{l}}^{M}} ),這樣就可以用上面語法 一節定義項的方式,遞迴地規定項的取值 :
元定義 — 在解釋 M {\displaystyle M} 下的某套變數取值下,一列項 T 1 , ⋯ , T n {\displaystyle T_{1},\,\cdots ,\,T_{n}} 的取值分別為 T 1 M , ⋯ , T n M {\displaystyle {T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M}} ,則這套變數取值下,項 f i n ( T 1 , ⋯ , T n ) {\displaystyle f_{i}^{n}(T_{1},\,\cdots ,\,T_{n})} 的取值規定為
( f i n ) M ( T 1 M , ⋯ , T n M ) {\displaystyle {(f_{i}^{n})}^{M}({T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M})} 直觀上要解釋關係最直接的方法,就是列舉所有符合關係的對象;例如如果想說明夫妻關係 ,可以列舉所有(老公, 老婆)的雙元有序對 ,但並非所有的人類有序對都會在這個關係中。
以此為基礎,若以 D m {\displaystyle D^{m}} 代表所有以 m {\displaystyle m} 個 D {\displaystyle D} 中的元素構成的 m {\displaystyle m} 元有序對的集合(也就是 m {\displaystyle m} 元笛卡兒積 ) ,那一套解釋 M {\displaystyle M} 會將 m {\displaystyle m} 元斷言符號 A j m {\displaystyle A_{j}^{m}} 解釋為一個
( A j m ) M ⊆ D m {\displaystyle {(A_{j}^{m})}^{M}\subseteq D^{m}} 的 m {\displaystyle m} 元有序對 子集合。
這樣就可以依據語法的遞迴定義,以下面的規則對每條公式賦予真值。(這種賦值方式稱為T-模式 ,取名於邏輯學家阿尔弗雷德·塔斯基)
元定義 — 在一套解釋 M {\displaystyle M} 下:
在一套特定的變數取值下,一列項 T 1 , ⋯ , T m {\displaystyle T_{1},\,\cdots ,\,T_{m}} 的取值為 T 1 M , ⋯ , T m M {\displaystyle {T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M}} ,那 A j m ( T 1 , ⋯ , T m ) {\displaystyle A_{j}^{m}(T_{1},\,\cdots ,\,T_{m})} 為真定義為 ( T 1 M , ⋯ , T m M ) ∈ ( A j m ) M {\displaystyle ({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\in {(A_{j}^{m})}^{M}} 反之 ( T 1 M , ⋯ , T m M ) ∉ ( A j m ) M {\displaystyle ({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\notin {(A_{j}^{m})}^{M}} 則定義為假。 在一套特定的變數取值下,「 ( ¬ B ) {\displaystyle (\neg {\mathcal {B}})} 為真」 等價於 「 B {\displaystyle {\mathcal {B}}} 為假」。 在一套特定的變數取值下, ( B ⇒ C ) {\displaystyle ({\mathcal {B}}\Rightarrow {\mathcal {C}})} 為真,意為「 B {\displaystyle {\mathcal {B}}} 為假或是 C {\displaystyle {\mathcal {C}}} 為真。」 (p =>q 為假只有p 為真且q 為假的狀況) 在變數取值 ⟨ a k ⟩ k ∈ N {\displaystyle \left\langle a_{k}\right\rangle _{k\in \mathbb {N} }} 下, ( ∀ x i B ) {\displaystyle (\forall x_{i}{\mathcal {B}})} 為真,意為「對所有的 d ∈ D {\displaystyle d\in D} , B {\displaystyle {\mathcal {B}}} 於變數取值 ⟨ a 1 , ⋯ , a i − 1 , d , a i + 1 , ⋯ ⟩ {\displaystyle \left\langle a_{1},\,\cdots ,\,a_{i-1},\,d,\,a_{i+1},\,\cdots \right\rangle } 下為真」。(也就是把變數 x i {\displaystyle x_{i}} 的取值換為論域的任意元素仍然為真) 更進一步的來說
另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數 擴展而成。有如下幾種類型:
這些代數 都是純粹擴展兩元素布林代數 而成的格 。
塔斯基和葛范德於1987年證明,沒有超過包在三個以上的量化內的原子句子 的部份一階邏輯,其表示力和關係代數 相同。上述部份一階邏輯令人十分地感到有興趣,因為它已足夠表示皮亞諾算術 和公理化集合論 ,包括典型的ZFC 。他們亦證明了,具有簡單有序對的一階邏輯和具有兩個有序的投影函數 的關係代數等價。
上述的語義解釋都要求論域為非空集合。但在如自由邏輯 之中,設定空論域是被允許的。甚至代數結構的類包含一個空結構(如空偏序集 ),當允許空論域時,這個類只能是一階邏輯中的一個基本類,不然就要將空結構由類中移除。
不過,空論域存在著一些難點:
許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為,當x 不是 ϕ {\displaystyle \phi \,} 內的自由變數時, ϕ ∨ ∃ x ψ {\displaystyle \phi \lor \exists x\psi } 會薀涵 ∃ x ( ϕ ∨ ψ ) {\displaystyle \exists x(\phi \lor \psi )} 。這個用來將公式寫成前束範式 的規則在非空論域中是可靠的,但在允許空論域時則是不可靠的。 在使用變數賦值函數的解釋中,真值的定義不能和空論域一起運作,因為不存在範圍為空的變數賦值函數。(相似地,也無法將解釋賦予上常數符號。)在甚至是原子公式的真值可被定義之前,都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值,且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作;除非將其改成配上空論域。 因此,若空論域是被允許的,通常也必須被視成特例。不過,大多數的作家會簡單地將空論域由定義中排除。
以下介紹一些基本用語和符號
口語上會稱公式 A {\displaystyle {\mathcal {A}}} (或 ⊢ L A {\displaystyle \vdash _{\mathcal {L}}{\mathcal {A}}} ) 為 L {\displaystyle {\mathcal {L}}} 下的定理 (theorem)。而這列 C i ( 1 ≤ i ≤ n ) {\displaystyle {\mathcal {C}}_{i}\,\,(1\leq i\leq n)} 會稱為 ⊢ L A {\displaystyle \vdash _{\mathcal {L}}{\mathcal {A}}} 的證明 。
例如定理 ( I ) {\displaystyle (I)} ⊢ L B ⇒ B {\displaystyle \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {B}}} 的證明:
以上其實是蘊含了無限多定理的元定理 的證明(因為沒有給出合式公式的明確形式)。方便起見,這種元定理 還是會稱為定理並以同樣的形式來表達。
直觀上的證明,總是會有一些“前提假設”,對此,若以 Γ {\displaystyle \Gamma } 代表一列有限數目的公式,那
這樣稱 C i ( 1 ≤ i ≤ n ) {\displaystyle {\mathcal {C}}_{i}\,\,(1\leq i\leq n)} 為在前提 Γ {\displaystyle \Gamma } 下, A {\displaystyle {\mathcal {A}}} 的證明 ;或是說 A {\displaystyle {\mathcal {A}}} 是 Γ {\displaystyle \Gamma } 的推論結果 。
若要特別凸顯 Γ {\displaystyle \Gamma } 裡的一條"前提條件" B {\displaystyle {\mathcal {B}}} 對"證明過程"的重要性,可以用 Γ , B ⊢ L A {\displaystyle \Gamma ,\,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {A}}} 的符號去特別凸顯。若 Γ {\displaystyle \Gamma } 裡的公式列舉出來有 B 1 , . . . , B n {\displaystyle {\mathcal {B}}_{1},...,{\mathcal {B}}_{n}} ,那亦可表示為
B 1 , . . . , B n ⊢ L A {\displaystyle {\mathcal {B}}_{1},...,{\mathcal {B}}_{n}\vdash _{\mathcal {L}}{\mathcal {A}}} 證明過程沒有被引用的公式盡可能不寫出來。另一方面從以上對於證明定義可以發現,依怎樣的順序列舉前提條件,對於證明本身是不會有任何影響的。
本節所介紹的符號,在引用哪個理論很顯然的情況下, ⊢ L {\displaystyle \vdash _{\mathcal {L}}} 的下標 L {\displaystyle {\mathcal {L}}} 可以省略。
實際的證明常常會"引用"別的(元)定理,嚴格來說,就是照抄(元)定理的證明過程,然後作一些修改使符號一致。為了節省證明的篇幅,引用時只會單單列出配合引用(元)定理所得出的公式(形式),並在後面註明引用的(元)定理代號。
從公理(A1)和(A2)會得出不但直觀且實用的演繹元定理 :
因為 Γ {\displaystyle \Gamma } 代表的是有限條公式,所以透過演繹元定理可以將證明過程必要的前提條件遞迴地移到 ⊢ {\displaystyle \vdash } 後,直到不需要任何前提為止;然後由MP律可以知道,若有 Γ ⊢ L B ⇒ C {\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}} ,則有 Γ , B ⊢ L C {\displaystyle \Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}} ,如此一來透過演繹元定理搬到推論結果的合式公式,也可以任意的搬回來。所以 Γ ⊢ L B {\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}} 等價於某定理 ⊢ L C {\displaystyle \vdash _{\mathcal {L}}{\mathcal {C}}} 。因此也會將 Γ ⊢ L B {\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}} 稱為一個定理 。
而從演繹元定理和MP律,會有以下直觀且實用的元定理
元定理 — (D1) D 1 ⇒ D 2 , D 2 ⇒ D 3 ⊢ D 1 ⇒ D 3 {\displaystyle {\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}
(D2) D 1 ⇒ ( D 2 ⇒ D 3 ) , D 2 ⊢ D 1