一階邏輯 是使用於數學 、哲學 、語言學 及電腦科學 中的一種形式系統 ,也可以稱為:一階斷言演算 、低階斷言演算 、量化理論 或謂詞邏輯 。一階邏輯和命題邏輯 的不同之處在於,一階邏輯包含量詞 。
高階邏輯 和一階邏輯不同之處在於,高階邏輯的斷言符號可以有斷言符號或函數符號當做引數 ,且容許斷言量詞或函數量詞[ 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
⇒
D
3
{\displaystyle {\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}}
以下如果需要將參照的定理以演繹元定理進行"搬移",會省略掉搬移的過程並在搬移後得到的結果後標註(D)。如果參照以上的(D1)和(D2)也會省略過程,單有結果和代號標註。
以下的證明會分成使用(A3)的部分跟將公理(A3)取代為(T1)的部分,用以證明兩者的等價性。
(DNe) Double negation, elimination —
⊢
¬
¬
A
⇒
A
{\displaystyle \vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
證明(使用A3)
(1)
(
¬
A
⇒
¬
¬
A
)
⇒
[
(
¬
A
⇒
¬
A
)
⇒
A
]
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}]}
(A3)
(2)
¬
A
⇒
¬
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}}
(I)
(3)
(
¬
A
⇒
¬
¬
A
)
⇒
A
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}}
(D2 with 1, 2)
(4)
¬
¬
A
⇒
(
¬
A
⇒
¬
¬
A
)
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})}
(A1)
(5)
¬
¬
A
⇒
A
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(D1 with 3, 4)
證明(使用T1)
(1)
¬
¬
A
⇒
(
¬
¬
¬
¬
A
⇒
¬
¬
A
)
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow (\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})}
(A1)
(2)
¬
¬
A
{\displaystyle \neg \neg {\mathcal {A}}}
(Hyp)
(3)
¬
¬
¬
¬
A
⇒
¬
¬
A
{\displaystyle \neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 2, 1)
(4)
¬
A
⇒
¬
¬
¬
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg \neg \neg {\mathcal {A}}}
(MP with 3, T1)
(5)
¬
¬
A
⇒
A
{\displaystyle \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(MP with 4, T1)
(6)
A
{\displaystyle {\mathcal {A}}}
(MP with 2, 5)
(DNi) Double negation, introduction —
⊢
A
⇒
¬
¬
A
{\displaystyle \vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
證明(使用A3)
(1)
(
¬
¬
¬
A
⇒
¬
A
)
⇒
[
(
¬
¬
¬
A
⇒
A
)
⇒
¬
¬
A
]
{\displaystyle (\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}]}
(A3)
(2)
(
¬
¬
¬
A
⇒
A
)
⇒
¬
¬
A
{\displaystyle (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}}
(MP with DNe, 1)
(3)
A
⇒
(
¬
¬
¬
A
⇒
A
)
{\displaystyle {\mathcal {A}}\Rightarrow (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})}
(A1)
(4)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(D1 with 2,3)
證明(使用T1)
(1)
¬
¬
¬
A
⇒
¬
A
{\displaystyle \neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}}
(DNe)
(2)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 1, T1)
上面兩定理表達了雙否定推理上等價於於原公式,參照兩者任一會都以(DN)簡寫。
(T1) Transposition-1 —
¬
A
⇒
¬
B
⊢
B
⇒
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}}
證明(使用A3)
(1)
(
¬
A
⇒
¬
B
)
⇒
[
(
¬
A
⇒
B
)
⇒
A
]
{\displaystyle (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}]}
(A3)
(2)
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(Hyp)
(3)
(
¬
A
⇒
B
)
⇒
A
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}}
(MP with 1, 2)
(4)
B
⇒
(
¬
A
⇒
B
)
{\displaystyle {\mathcal {B}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})}
(A1)
(5)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(D1 with 3, 4)
(T2) Transposition-2 —
B
⇒
A
⊢
¬
A
⇒
¬
B
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
證明(使用T1)
(1)
¬
¬
B
⇒
B
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}}
(DN)
(2)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(Hyp)
(3)
¬
¬
B
⇒
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(D with 1, 2)
(4)
A
⇒
¬
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
(DN)
(5)
¬
¬
B
⇒
¬
¬
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}}
(D1 with 3,4)
(6)
(
¬
¬
B
⇒
¬
¬
A
)
⇒
(
¬
A
⇒
¬
B
)
{\displaystyle (\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(T1, D)
(7)
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(MP with 5, 6)
注意到(T2)的證明參照了(T1)+(DN),但之前已經證明了(A1)+(A2)+(A3)可以推出(T1);還有(A1)+(A2)+(T1)也可以推出(DN),所以註明使用(T1)即可。
以上二定理說明
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
推理上等價於
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
,參照這兩個定理中任一都以(T)表示。
至此,已經可以證明(A1)+(A2)+(T1)可以推出(A3):
(T1)可推出(A3)的證明
由MP律 顯然有
¬
B
,
(
¬
B
⇒
B
)
⊢
B
{\displaystyle \neg {\mathcal {B}},\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {B}}}
(1)
¬
B
⇒
[
(
¬
B
⇒
B
)
⇒
B
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}\,]}
(對上面的定理使用兩次演繹元定理)
(2)
¬
B
⇒
[
¬
B
⇒
¬
(
¬
B
⇒
B
)
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]}
(D1 with 1, T2)
(3)
(
¬
B
⇒
¬
B
)
⇒
[
¬
B
⇒
¬
(
¬
B
⇒
B
)
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]}
(MP with A2, 2)
(4)
¬
B
⇒
¬
(
¬
B
⇒
B
)
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})}
(MP with I, 3)
(5)
(
¬
B
⇒
B
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}}
(MP with T1, 4)
(6)
(
¬
B
)
⇒
(
¬
C
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})}
(Hyp)
(7)
¬
B
⇒
C
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(8)
¬
C
⇒
¬
¬
B
{\displaystyle \neg {\mathcal {C}}\Rightarrow \neg \neg {\mathcal {B}}}
(MP with T2, 7)
(9)
¬
B
⇒
¬
¬
B
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {B}}}
(D1 with 6, 8)
(10)
¬
B
⇒
B
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}}
(D1 with DN, 9)
(11)
B
{\displaystyle {\mathcal {B}}}
(MP with 5, 10)
所以綜合以上所述,在有(A1)+(A2)的前提下,公理(T1)等價於公理(A3)。
由(T)可以得到類似於公理(A3)的定理
(A3') —
A
⇒
B
,
¬
A
⇒
B
⊢
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}}
證明
(1)
(
¬
B
⇒
¬
¬
A
)
⇒
[
(
¬
B
⇒
¬
A
)
⇒
B
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
(A3)
(2)
(
¬
A
⇒
B
)
⇒
(
¬
B
⇒
¬
¬
A
)
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})}
(T, D)
(3)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(4)
¬
B
⇒
¬
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}}
(MP with 2, 3)
(5)
(
¬
B
⇒
¬
A
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}}
(MP with 1, 4)
(6)
(
A
⇒
B
)
⇒
(
¬
B
⇒
¬
A
)
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(T, D)
(7)
A
⇒
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(8)
¬
B
⇒
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 6, 7)
(9)
B
{\displaystyle {\mathcal {B}}}
(MP with 5, 8)
以下的定理重現了實質條件 的直觀理解。
(M0)material condition —
¬
A
,
A
⊢
B
{\displaystyle \neg {\mathcal {A}},{\mathcal {A}}\vdash {\mathcal {B}}}
(也就是
¬
A
⊢
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}}
)
證明
(1)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(Hyp)
(2)
A
{\displaystyle {\mathcal {A}}}
(Hyp)
(3)
(
¬
B
⇒
¬
A
)
⇒
[
(
¬
B
⇒
A
)
⇒
B
]
{\displaystyle (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}]}
(A3)
(4)
¬
A
⇒
(
¬
B
⇒
¬
A
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(A1)
(5)
¬
B
⇒
¬
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 4, 1)
(6)
A
⇒
(
¬
B
⇒
A
)
{\displaystyle {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})}
(A1)
(7)
¬
B
⇒
A
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(MP with 6, 2)
(8)
(
¬
B
⇒
A
)
⇒
B
{\displaystyle (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}}
(MP with 3,5)
(9)
B
{\displaystyle {\mathcal {B}}}
(MP with 8,7)
(M1)material condition —
A
,
¬
B
⊢
¬
(
A
⇒
B
)
{\displaystyle {\mathcal {A}},\neg {\mathcal {B}}\vdash \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
證明
首先注意到
A
,
A
⇒
B
⊢
B
{\displaystyle {\mathcal {A}},{\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}}
(MP)
(1)
A
⇒
[
(
A
⇒
B
)
⇒
B
]
{\displaystyle {\mathcal {A}}\Rightarrow [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]}
(0, D)
(2)
[
(
A
⇒
B
)
⇒
B
]
⇒
{
¬
B
⇒
[
¬
(
A
⇒
B
)
]
}
{\displaystyle [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\Rightarrow \{\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\}}
(T)
(3)
A
{\displaystyle {\mathcal {A}}}
(Hyp)
(4)
(
A
⇒
B
)
⇒
B
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}}
(MP with 1, 3)
(5)
¬
B
⇒
[
¬
(
A
⇒
B
)
]
{\displaystyle \neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]}
(MP with 2, 4)
(6)
¬
B
{\displaystyle \neg {\mathcal {B}}}
(Hyp)
(7)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(MP 5, 6)
(M2)material condition —
¬
(
A
⇒
B
)
⊢
¬
B
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash \neg {\mathcal {B}}}
證明
(1)
B
⇒
(
A
⇒
B
)
{\displaystyle {\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(A1)
(2)
[
B
⇒
(
A
⇒
B
)
]
⇒
{
[
¬
(
A
⇒
B
)
]
⇒
(
¬
B
)
}
{\displaystyle [{\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})\}}
(T)
(3)
[
¬
(
A
⇒
B
)
]
⇒
(
¬
B
)
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})}
(MP with 1, 2)
(4)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(Hyp)
(5)
¬
B
{\displaystyle \neg {\mathcal {B}}}
(MP with 3, 4)
(M3)material condition —
¬
(
A
⇒
B
)
⊢
A
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {A}}}
證明
(1)
¬
A
⇒
(
A
⇒
B
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(M0, D)
(2)
[
¬
A
⇒
(
A
⇒
B
)
]
⇒
{
[
¬
(
A
⇒
B
)
]
⇒
(
¬
¬
A
)
}
{\displaystyle [\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})\}}
(T)
(3)
[
¬
(
A
⇒
B
)
]
⇒
(
¬
¬
A
)
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})}
(MP with 1, 2)
(4)
¬
(
A
⇒
B
)
{\displaystyle \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(Hyp)
(5)
¬
¬
A
{\displaystyle \neg \neg {\mathcal {A}}}
(MP with 3,4)
(6)
A
{\displaystyle {\mathcal {A}}}
(MP with 5, DN)
(C1)Proof by Contradiction —
A
⇒
¬
B
,
B
⊢
¬
A
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}},{\mathcal {B}}\vdash \neg {\mathcal {A}}}
證明
(1)
(
A
⇒
¬
B
)
⇒
(
¬
¬
B
⇒
¬
A
)
{\displaystyle ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow (\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})}
(T, D)
(2)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(Hyp)
(3)
¬
¬
B
⇒
¬
A
{\displaystyle \neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}}
(MP with 1, 2)
(4)
B
{\displaystyle {\mathcal {B}}}
(Hyp)
(5)
¬
¬
B
{\displaystyle \neg \neg {\mathcal {B}}}
(MP with DN, 4)
(6)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(MP with 3, 5)
(C2)Proof by Contradiction —
¬
A
⇒
B
,
¬
B
⊢
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}}
以下為邏輯與 的交換性
元定理 —
⊢
(
A
∧
B
)
⇒
(
B
∧
A
)
{\displaystyle \vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow ({\mathcal {B}}\wedge {\mathcal {A}})}
證明
(1)
(
B
⇒
¬
A
)
⇒
(
A
⇒
¬
B
)
{\displaystyle ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(C1, D)
(2)
[
(
B
⇒
¬
A
)
⇒
(
A
⇒
¬
B
)
]
⇒
{
[
¬
(
A
⇒
¬
B
)
]
⇒
[
¬
(
B
⇒
¬
A
)
]
}
{\displaystyle [({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]\}}
(T, D)
(3)
[
¬
(
A
⇒
¬
B
)
]
⇒
[
¬
(
B
⇒
¬
A
)
]
{\displaystyle [\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]}
(MP with 1,2)
類似的,(C2)正是邏輯或 的交換性:
元定理 —
A
∨
B
⊢
B
∨
A
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {B}}\vee {\mathcal {A}}}
(C2, D)
"且"的直觀意義是實質條件元定理的直接結果
(AND)Intuitive meaning of And —
A
,
B
⊢
A
∧
B
{\displaystyle {\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}}
(M1)
A
∧
B
⊢
A
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}}
(M3)
A
∧
B
⊢
B
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}}
(M2)
從(AND)和
⇔
{\displaystyle \Leftrightarrow }
的符號定義可知,
⊢
B
⇔
C
{\displaystyle \vdash {\mathcal {B}}\Leftrightarrow {\mathcal {C}}}
的證明可以拆成兩部分;習慣上會以「(
⇒
{\displaystyle \Rightarrow }
) 」標示
⊢
B
⇒
C
{\displaystyle \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}}
部分的證明,而「(
⇐
{\displaystyle \Leftarrow }
) 」標示
⊢
C
⇒
B
{\displaystyle \vdash {\mathcal {C}}\Rightarrow {\mathcal {B}}}
部分的證明。
類似的,"或"的直觀意義是(M0)跟(D)的直截結果
(OR)Intuitive meaning of OR —
A
⊢
A
∨
B
{\displaystyle {\mathcal {A}}\vdash {\mathcal {A}}\vee {\mathcal {B}}}
(M0, DN)
B
⊢
A
∨
B
{\displaystyle {\mathcal {B}}\vdash {\mathcal {A}}\vee {\mathcal {B}}}
(A1, D)
A
∨
B
,
¬
A
⊢
B
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {A}}\vdash {\mathcal {B}}}
(D)
A
∨
B
,
¬
B
⊢
A
{\displaystyle {\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}}
(交換性, D)
以下的定理則是(A3')的直截結果
(DisJ)Disjunction —
A
⇒
C
,
B
⇒
C
,
A
∨
B
⊢
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}},{\mathcal {B}}\Rightarrow {\mathcal {C}},{\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {C}}}
證明
(1)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(Hyp)
(2)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 1, 2)
(4)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(Hyp)
(5)
C
{\displaystyle {\mathcal {C}}}
(A3' with 3, 4)
對於"且",展開符號定義後,可以從直觀意義輕鬆地得到
(ASO-AND)Associativity of AND —
⊢
A
∧
(
B
∧
C
)
⇔
(
A
∧
B
)
∧
C
{\displaystyle \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\wedge {\mathcal {C}}}
"或"也有類似的性質
(ASO-OR)Associativity of OR —
⊢
A
∨
(
B
∨
C
)
⇔
(
A
∨
B
)
∨
C
{\displaystyle \vdash {\mathcal {A}}\vee ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\vee {\mathcal {C}}}
"且"和"或"之間還有分配律
(DIS-1)Distribution —
⊢
A
∧
(
B
∨
C
)
⇔
(
A
∧
B
)
∨
(
A
∧
C
)
{\displaystyle \vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})}
證明
(
⇒
{\displaystyle \Rightarrow }
)
(1)
A
∧
(
B
∨
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(Hyp)
(2)
A
{\displaystyle {\mathcal {A}}}
(MP with 1, AND)
(3)
¬
B
⇒
C
{\displaystyle \neg {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(MP with 1, AND)
(4)
¬
¬
(
A
⇒
¬
B
)
{\displaystyle \neg \neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})}
(Hyp)
(5)
A
⇒
¬
B
{\displaystyle {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
(MP with 4, DN)
(6)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 3, 5)
(7)
C
{\displaystyle {\mathcal {C}}}
(MP with 2, 5)
(8)
A
∧
C
{\displaystyle {\mathcal {A}}\wedge {\mathcal {C}}}
(MP twice with 2, 7, AND)
也就是
A
∧
(
B
∨
C
)
,
¬
(
A
∧
B
)
⊢
A
∧
C
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg ({\mathcal {A}}\wedge {\mathcal {B}})\vdash {\mathcal {A}}\wedge {\mathcal {C}}}
再套用(D)就會得到
A
∧
(
B
∨
C
)
⊢
(
A
∧
B
)
∨
(
A
∧
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})}
(
⇐
{\displaystyle \Leftarrow }
)
(1)
¬
(
A
∧
B
)
⇒
A
∧
C
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}\wedge {\mathcal {C}}}
(Hyp)
(2)
¬
(
A
∧
B
)
⇒
A
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}}
(D1 with 1, AND)
(3)
¬
(
A
∧
B
)
⇒
C
{\displaystyle \neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}}
(D1 with 1, AND)
(4)
¬
A
⇒
(
A
∧
B
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with 2, C2)
(5)
¬
C
⇒
(
A
∧
B
)
{\displaystyle \neg {\mathcal {C}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})}
(MP with 3, C2)
(6)
¬
A
⇒
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
(D1 with 4, AND)
(7)
¬
C
⇒
B
{\displaystyle \neg {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(D1 with 4, AND)
(8)
A
{\displaystyle {\mathcal {A}}}
(A3' with 6, I)
(9)
A
∧
(
B
∨
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(MP twice with 7, 8, AND)
也就是
(
A
∧
B
)
∨
(
A
∧
C
)
⊢
A
∧
(
B
∨
C
)
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})}
(DIS-2)Distribution —
⊢
A
∨
(
B
∧
C
)
⇔
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle \vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
證明
(
⇒
{\displaystyle \Rightarrow }
)
(1)
¬
A
⇒
(
B
∧
C
)
{\displaystyle \neg {\mathcal {A}}\Rightarrow ({\mathcal {B}}\wedge {\mathcal {C}})}
(Hyp)
(2)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(D1 with 1, AND)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(D1 with 1, AND)
(4)
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
(MP twice with 2, 3,AND)
也就是
A
∨
(
B
∧
C
)
⊢
(
A
∨
B
)
∧
(
A
∨
C
)
{\displaystyle {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\vdash ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})}
(
⇐
{\displaystyle \Leftarrow }
)
(1)
(
¬
A
⇒
B
)
∧
(
¬
A
⇒
C
)
{\displaystyle (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge (\neg {\mathcal {A}}\Rightarrow {\mathcal {C}})}
(Hyp)
(2)
¬
A
⇒
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(MP with 1, AND)
(3)
¬
A
⇒
C
{\displaystyle \neg {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(MP with 1, AND)
(4)
¬
A
{\displaystyle \neg {\mathcal {A}}}
(Hyp)
(5)
B
{\displaystyle {\mathcal {B}}}
(MP with 2,4)
(6)
C
{\displaystyle {\mathcal {C}}}
(MP with 3,4)
(7)
B
∧
C
{\displaystyle {\mathcal {B}}\wedge {\mathcal {C}}}
(MP twice with 5, 6, AND)
也就是
A
∧
(
B
∨
C
)
,
¬
A
⊢
B
∧
C
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg {\mathcal {A}}\vdash {\mathcal {B}}\wedge {\mathcal {C}}}
再使用一次推論元定理會得到
A
∧
(
B
∨
C
)
⊢
A
∨
(
B
∧
C
)
{\displaystyle {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})}
以下的元定理的名字來自於英國邏輯學家奧古斯塔斯·德摩根 。
De Morgan I —
⊢
[
¬
(
A
∧
B
)
]
⇔
[
(
¬
A
)
∨
(
¬
B
)
]
{\displaystyle \vdash [\neg ({\mathcal {A}}\wedge {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\vee (\neg {\mathcal {B}})]}
De Morgan II —
⊢
[
¬
(
A
∨
B
)
]
⇔
[
(
¬
A
)
∧
(
¬
B
)
]
{\displaystyle \vdash [\neg ({\mathcal {A}}\vee {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})]}
公理模式 (A7)可以稍加延伸成以下的元定理
定理的普遍化 —
對任意變量
x
{\displaystyle x}
,若
⊢
B
{\displaystyle \vdash {\mathcal {B}}}
則有
⊢
(
∀
x
)
B
{\displaystyle \vdash (\forall x){\mathcal {B}}}
。
更進一步,有以下元定裏
(GEN) —
在
A
1
,
A
2
,
.
.
.
.
,
A
n
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}}
裏變量
x
{\displaystyle x}
都完全被約束,若
A
1
,
A
2
,
.
.
.
.
,
A
n
⊢
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash {\mathcal {B}}}
則有
A
1
,
A
2
,
.
.
.
.
,
A
n
⊢
(
∀
x
)
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash (\forall x){\mathcal {B}}}
證明
以下對前提條件的數量
n
{\displaystyle n}
做歸納。
若
n
=
1
{\displaystyle n=1}
,根據前提有
A
1
⊢
B
{\displaystyle {\mathcal {A}}_{1}\vdash {\mathcal {B}}}
以(D)將
A
1
{\displaystyle {\mathcal {A}}_{1}}
往前搬,再套用定理的普遍化,會得到
⊢
(
∀
x
)
(
A
1
⇒
B
)
{\displaystyle \vdash (\forall x)({\mathcal {A}}_{1}\Rightarrow {\mathcal {B}})}
再根據(A5)和MP律,就可以得到
⊢
A
1
⇒
(
∀
x
)
B
{\displaystyle \vdash {\mathcal {A}}_{1}\Rightarrow (\forall x){\mathcal {B}}}
也就是本元定理要求的結果。
現在假設
n
<
k
{\displaystyle n<k}
的情況下元定理會成立。元定理的前提條件根據(D)可以寫為
A
1
,
A
2
,
.
.
.
.
,
A
k
−
1
⊢
A
k
⇒
B
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash {\mathcal {A}}_{k}\Rightarrow {\mathcal {B}}}
則根據歸納法的假設
A
1
,
A
2
,
.
.
.
.
,
A
k
−
1
⊢
(
∀
x
)
(
A
k
⇒
B
)
{\displaystyle {\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash (\forall x)({\mathcal {A}}_{k}\Rightarrow {\mathcal {B}})}
上式配上(A5),本元定理在
n
=
k
{\displaystyle n=k}
的情況就可以得到證明,故本元定理得證。
◻
{\displaystyle \Box }
(GEN)可以稍加修飾,以套用在含有存在量詞的公式上
以下的定理,說明兩條「等價」的公式可以互相代換
證明
以下的證明都會用到這三條公式:
(a)
A
⇔
B
{\displaystyle {\mathcal {A}}\Leftrightarrow {\mathcal {B}}}
(from
Γ
{\displaystyle \Gamma }
)
(b)
A
⇒
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}
(MP with AND , a)
(c)
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
(MP with AND , a)
1.
(1)
(
¬
B
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , b)
(2)
(
¬
A
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , c)
(3)
(
¬
A
)
⇔
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})}
(AND with 3, 5)
2.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
C
⇒
A
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {A}}}
(Hyp)
(2)
C
⇒
B
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(D1 with 1, b)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
C
⇒
B
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {B}}}
(Hyp)
(2)
C
⇒
A
{\displaystyle {\mathcal {C}}\Rightarrow {\mathcal {A}}}
(D1 with 1, c)
3.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(Hyp)
(2)
(
¬
C
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , 1)
(3)
(
¬
A
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , c)
(4)
(
¬
C
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})}
(D1 with 2, 3)
(5)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(MP with T , 4)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
B
⇒
C
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {C}}}
(Hyp)
(2)
(
¬
C
)
⇒
(
¬
B
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})}
(MP with T , 1)
(3)
(
¬
B
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})}
(MP with T , b)
(4)
(
¬
C
)
⇒
(
¬
A
)
{\displaystyle (\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})}
(D1 with 2, 3)
(5)
A
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {C}}}
(MP with T , 4)
4.
(
⇒
{\displaystyle \Rightarrow }
)
(1)
(
∀
x
)
(
A
⇒
B
)
{\displaystyle (\forall x)({\mathcal {A}}\Rightarrow {\mathcal {B}})}
(GEN with
x
{\displaystyle x}
, a)
(2)
(
∀
x
)
A
⇒
(
∀
x
)
B
{\displaystyle (\forall x){\mathcal {A}}\Rightarrow (\forall x){\mathcal {B}}}
(MP with A6 , 1)
(
⇐
{\displaystyle \Leftarrow }
)
(1)
(
∀
x
)
(
B
⇒
A
)
{\displaystyle (\forall x)({\mathcal {B}}\Rightarrow {\mathcal {A}})}
(GEN with
x
{\displaystyle x}
, c)
(2)
(
∀
x
)
B
⇒
(
∀
x
)
A
{\displaystyle (\forall x){\mathcal {B}}\Rightarrow (\forall x){\mathcal {A}}}
(MP with A6 , 1)
這些定理通常是混合使用,以達到「等價代換」的結果,例如,考慮到「邏輯與」是以下的符號定義:
(
A
∧
C
)
:=
¬
[
A
⇒
(
¬
C
)
]
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {C}}):=\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]}
那如果假設
⊢
A
⇔
B
{\displaystyle \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}}
,就有:
⊢
[
A
⇒
(
¬
C
)
]
⇔
[
B
⇒
(
¬
C
)
]
{\displaystyle \vdash [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]}
⊢
¬
[
A
⇒
(
¬
C
)
]
⇔
{
¬
[
B
⇒
(
¬
C
)
]
}
{\displaystyle \vdash \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow \{\neg [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]\}}
換句話說,從「
⊢
A
⇔
B
{\displaystyle \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}}
」可以得到「
⊢
(
A
∧
C
)
⇔
(
B
∧
C
)
{\displaystyle \vdash ({\mathcal {A}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\wedge {\mathcal {C}})}
」,直觀上相當於,把
A
{\displaystyle {\mathcal {A}}}
都代換成
B
{\displaystyle {\mathcal {B}}}
則兩式等價。日後像這樣遞歸地套用上述定理來得到「代換則某兩式等價」,都簡單地以「參照(Equv)」來表示這段實際的推演過程。
由普遍化,很容易證明以下關於"交換性"的定理
元定理 —
(1)
(
∀
x
)
(
∀
y
)
A
⊢
(
∀
y
)
(
∀
x
)
A
{\displaystyle (\forall x)(\forall y){\mathcal {A}}\vdash (\forall y)(\forall x){\mathcal {A}}}
(2)
(
∃
x
)
(
∃
y
)
A
⊢
(
∃
y
)
(
∃
x
)
A
{\displaystyle (\exists x)(\exists y){\mathcal {A}}\vdash (\exists y)(\exists x){\mathcal {A}}}
(3)
(
∃
x
)
(
∀
y
)
A
⊢
(
∀
y
)
(
∃
x
)
A
{\displaystyle (\exists x)(\forall y){\mathcal {A}}\vdash (\forall y)(\exists x){\mathcal {A}}}
注意最後(3)一般來說是不能反向的,只要想到"對每個
a
{\displaystyle a}
,都有一個數(也就是
−
a
{\displaystyle -a}
),使
a
+
(
−
a
)
=
0
{\displaystyle a+(-a)=0}
",但是任取一個
a
{\displaystyle a}
的數
(
−
a
)
{\displaystyle (-a)}
和任意的數
b
{\displaystyle b}
,
b
+
(
−
a
)
{\displaystyle b+(-a)}
並不一定會為零。
數學中常常有 "對所有
ϵ
>
0
{\displaystyle \epsilon >0}
有...",或是 "存在
δ
>
0
{\displaystyle \delta >0}
使的..."。而兩句話比較清晰,接近一階邏輯語言的說法是 "對所有
ϵ
{\displaystyle \epsilon }
,只要
ϵ
>
0
{\displaystyle \epsilon >0}
則..." 與 "存在
δ
{\displaystyle \delta }
,
δ
>
0
{\displaystyle \delta >0}
且..."。「大於」直觀上是一個二元關係 ,也就是說,在公理化集合論 裏對應於一條
ϵ
{\displaystyle \epsilon }
( 或
δ
{\displaystyle \delta }
) 在裏面完全自由的合式公式。據此,可做以下的符號定義
符號定義 —
如果變量
x
{\displaystyle x}
和
y
{\displaystyle y}
都於合式公式
A
(
x
,
y
)
{\displaystyle {\mathcal {A}}(x,\,y)}
裏完全自由,那
[
∀
A
(
x
,
y
)
]
B
:=
(
∀
x
)
[
A
(
x
,
y
)
⇒
B
]
{\displaystyle [\,\forall {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\forall x)[\,{\mathcal {A}}(x,\,y)\Rightarrow {\mathcal {B}}\,]}
[
∃
A
(
x
,
y
)
]
B
:=
(
∃
x
)
[
A
(
x
,
y
)
∧
B
]
{\displaystyle [\,\exists {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\exists x)[\,{\mathcal {A}}(x,\,y)\wedge {\mathcal {B}}\,]}
但直觀上也會說 "對所有
n
>
0
{\displaystyle n>0}
和
m
>
0
{\displaystyle m>0}
有...",這樣連續,帶有條件的全稱量詞也是有"交換性"的。 為了討論這個問題,首先需要一些前置的定理
(abb) —
⊢
[
A
⇒
(
B
⇒
C
)
]
⇔
[
(
A
∧
B
)
⇒
C
]
{\displaystyle \vdash [{\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Leftrightarrow [({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}]}
證明
(
⇒
{\displaystyle \Rightarrow }
)
A
⇒
(
B
⇒
C
)
⊢
(
A
∧
B
)
⇒
C
{\displaystyle {\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}}
注意到
(AND)
A
∧
B
⊢
A
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}}
(AND)
A
∧
B
⊢
B
{\displaystyle {\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}}
所以
A
⇒
(
B
⇒
C
)
,
A
∧
B
⊢
C
{\displaystyle {\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}),\,{\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {C}}}
再套上演繹元定理 就可以得證。
◻
{\displaystyle \Box }
(
⇐
{\displaystyle \Leftarrow }
)
(
A
∧
B
)
⇒
C
⊢
A
⇒
(
B
⇒
C
)
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}\vdash {\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})}
注意到
(AND)
A
,
B
⊢
A
∧
B
{\displaystyle {\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}}
所以
(
A
∧
B
)
⇒
C
,
A
,
B
⊢
C
{\displaystyle ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}},\,{\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {C}}}
再套上演繹元定理 就可以得證。
◻
{\displaystyle \Box }
這樣就可以證明以下定理
元定理 —
如果變量
x
{\displaystyle x}
和
y
{\displaystyle y}
都於合式公式
A
(
x
,
y
)
{\displaystyle {\mathcal {A}}(x,\,y)}
和
B
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)}
裏完全自由,若項
T
{\displaystyle T}
裏沒有
y
{\displaystyle y}
那
⊢
[
∀
A
(
x
,
T
)
]
[
∀
B
(
y
,
S
)
]
C
⇔
∀
x
∀
y
{
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
C
}
{\displaystyle \vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow \forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {C}}\}}
證明
(
⇒
{\displaystyle \Rightarrow }
)
[
∀
A
(
x
,
T
)
]
[
∀
B
(
y
,
S
)
]
C
⊢
∀
x
∀
y
{
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
B
}
{\displaystyle [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\vdash \forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}}
(1)
(
∀
x
)
{
A
(
x
,
T
)
⇒
(
∀
y
)
[
B
(
y
,
S
)
⇒
C
]
}
{\displaystyle (\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}}
(Hyp)
(2)
A
(
x
,
T
)
⇒
(
∀
y
)
[
B
(
y
,
S
)
⇒
C
]
{\displaystyle {\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]}
(MP with 1, A4)
(3)
A
(
x
,
T
)
⇒
[
B
(
y
,
S
)
⇒
C
]
{\displaystyle {\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]}
(D1 with 2, A4)
(4)
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
C
{\displaystyle [\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {C}}}
(MP with abb, 3)
(5)
∀
x
∀
y
{
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
B
}
{\displaystyle \forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {B}}\}}
(GEN with 4 twice)
(
⇐
{\displaystyle \Leftarrow }
)
∀
x
∀
y
{
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
B
}
⊢
[
∀
A
(
x
,
T
)
]
[
∀
B
(
y
,
S
)
]
C
{\displaystyle \forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}}
(1)
∀
x
∀
y
{
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
B
}
{\displaystyle \forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}}
(Hyp)
(2)
[
A
(
x
,
T
)
∧
B
(
y
,
S
)
]
⇒
B
{\displaystyle [\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}}
(MP with 2, A4 twice)
(3)
A
(
x
,
T
)
⇒
[
B
(
y
,
S
)
⇒
C
]
{\displaystyle {\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]}
(MP with abb, 2)
(4)
(
∀
y
)
{
A
(
x
,
T
)
⇒
[
B
(
y
,
S
)
⇒
C
]
}
{\displaystyle (\forall y)\{\,{\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}}
(GEN with 3)
(5)
A
(
x
,
T
)
⇒
(
∀
y
)
[
B
(
y
,
S
)
⇒
C
]
{\displaystyle {\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]}
(MP with A5, 4)
(6)
(
∀
x
)
{
A
(
x
,
T
)
⇒
(
∀
y
)
[
B
(
y
,
S
)
⇒
C
]
}
{\displaystyle (\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}}
(GEN with 5)
如果再加上 "項
S
{\displaystyle S}
裏沒有
x
{\displaystyle x}
" 那就是 "對所有
n
>
0
{\displaystyle n>0}
和
m
>
0
{\displaystyle m>0}
有...",也就是以上所討論的情況了。以這個定理配上全稱量詞本身的交換性定理,那這句話就可以等價的說成 "對所有
m
{\displaystyle m}
和
n
{\displaystyle n}
若
n
>
0
{\displaystyle n>0}
且
m
>
0
{\displaystyle m>0}
則...",所以根據"且"的可交換性,可以進一步的說成 "對所有
m
>
0
{\displaystyle m>0}
和
n
>
0
{\displaystyle n>0}
有...",所以連續帶有條件的全稱量詞是"可交換的"。也就是說
元定理 —
如果變量
x
{\displaystyle x}
和
y
{\displaystyle y}
都於合式公式
A
(
x
,
y
)
{\displaystyle {\mathcal {A}}(x,\,y)}
和
B
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)}
裏完全自由,若項
T
{\displaystyle T}
裏沒有
y
{\displaystyle y}
,且項
S
{\displaystyle S}
裏沒有
x
{\displaystyle x}
則
⊢
[
∀
A
(
x
,
T
)
]
[
∀
B
(
y
,
S
)
]
C
⇔
[
∀
B
(
y
,
S
)
]
[
∀
A
(
x
,
T
)
]
C
{\displaystyle \vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow [\,\forall {\mathcal {B}}(y,\,S)\,][\,\forall {\mathcal {A}}(x,\,T)\,]{\mathcal {C}}}
但對於帶條件的存在量詞,首先可以得到以下非等價的定理。
元定理 —
(
∃
x
)
(
∃
y
)
(
A
∧
B
∧
C
)
⊢
(
∃
x
)
[
A
∧
(
∃
y
)
(
B
∧
C
)
]
{\displaystyle (\exists x)(\exists y)({\mathcal {A}}\wedge {\mathcal {B}}\wedge {\mathcal {C}})\vdash (\exists x)[\,{\mathcal {A}}\wedge (\exists y)({\mathcal {B}}\wedge {\mathcal {C}})\,]}
這是因為一般來說,
(
∃
y
)
D
{\displaystyle (\exists y){\mathcal {D}}}
不總是能推出
D
{\displaystyle {\mathcal {D}}}
。雖說如此,只要對公式做出一些限制,就會有以下交換的直觀定理:
證明
(
⇒
{\displaystyle \Rightarrow }
)
(1)
Q
⇒
(
∀
x
)
(
¬
R
)
{\displaystyle {\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})}
(Hyp)
(2)
Q
⇒
(
¬
R
)
{\displaystyle {\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})}
(D1 with 1 and A4 )
換句話說
Q
⇒
(
∀
x
)
(
¬
R
)
⊢
Q
⇒
(
¬
R
)
{\displaystyle {\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash {\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})}
這樣使用(GEN) 有
Q
⇒
(
∀
x
)
(
¬
R
)
⊢
(
∀
x
)
[
Q
⇒
(
¬
R
)
]
{\displaystyle {\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash (\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]}
這樣對上式使用(De Morgan) 和(T) 就有
⊢
(
∃
x
)
(
R
∧
Q
)
⇒
[
(
∃
x
)
(
R
)
∧
Q
)
]
{\displaystyle \vdash (\exists x)({\mathcal {R}}\wedge {\mathcal {\mathcal {Q}}})\Rightarrow [(\exists x)({\mathcal {R}})\wedge {\mathcal {Q}})]}
(
⇐
{\displaystyle \Leftarrow }
)
(1)
(
∀
x
)
[
Q
⇒
(
¬
R
)
]
⇒
[
Q
⇒
(
∀
x
)
(
¬
R
)
]
{\displaystyle (\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]\Rightarrow [{\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})]}
(A5)
(2)
(
∀
x
)
[
(
¬
Q
)
∨
(
¬
R
)
]
⇒
[
(
¬
Q
)
∨
(
∀
x
)
(
¬
R
)
]
{\displaystyle (\forall x)[(\neg {\mathcal {Q}})\vee (\neg {\mathcal {R}})]\Rightarrow [(\neg {\mathcal {Q}})\vee (\forall x)(\neg {\mathcal {R}})]}
(
∨
{\displaystyle \vee }
的定義 )
(3)
(
∀
x
)
[
¬
(
Q
∧
R
)
]
⇒
{
¬
[
(
Q
)
∨
(
∃
x
)
(
R
)
]
}
{\displaystyle (\forall x)[\neg ({\mathcal {Q}}\wedge {\mathcal {R}})]\Rightarrow \{\neg [({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\}}
(MP with 2, De Morgan )
(4)
[
(
Q
)
∨
(
∃
x
)
(
R
)
]
⇒
(
∃
x
)
(
Q
∧
R
)
{\displaystyle [({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\Rightarrow (\exists x)({\mathcal {Q}}\wedge {\mathcal {R}})}
(MP with 3, T )
也就是直觀上,「存在x使得 x>0 且 y>0」與「y>0 且存在x使得 x>0」是一樣的意思。
一般來說,等式
(
x
=
y
)
{\displaystyle (x=y)}
會被視為某個合式公式
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
的簡寫。若使用元定理的形式刻劃等式的性質,會作如下的定義
元定義 —
說一階邏輯理論
L
{\displaystyle {\mathcal {L}}}
帶相等符號
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
意為(
x
1
,
⋯
,
x
n
{\displaystyle x_{1},\,\cdots ,\,x_{n}}
、
x
{\displaystyle x}
和
y
{\displaystyle y}
都是
L
{\displaystyle {\mathcal {L}}}
的任意變量)
除了變量
x
{\displaystyle x}
和
y
{\displaystyle y}
於
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
是完全自由外其他變量都完全被約束
(E1)
⊢
L
E
(
x
,
x
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,x)}
。
(E2')
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
為
L
{\displaystyle {\mathcal {L}}}
內不含函數符號與常數符號的原子公式 ,
x
{\displaystyle x}
若以
B
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)}
表示
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
內某一個
x
{\displaystyle x}
被取代成
y
{\displaystyle y}
而成的新公式,則有
⊢
L
E
(
x
,
y
)
⇒
[
B
(
x
,
x
)
⇒
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]}
(E2") 若以
f
i
n
(
x
1
,
⋯
,
y
,
⋯
,
x
n
)
{\displaystyle f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})}
代表項
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
{\displaystyle f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})}
裏的
x
k
{\displaystyle x_{k}}
被取代成
y
{\displaystyle y}
而成的新項,則有
⊢
L
E
(
x
k
,
y
)
⇒
E
[
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
,
f
i
n
(
x
1
,
⋯
,
y
,
⋯
,
x
n
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]}
(E3)
⊢
L
E
(
x
,
y
)
⇒
E
(
y
,
x
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(y,\,x)}
。
並在這種狀況下,規定
(
x
=
y
)
{\displaystyle (x=y)}
為
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
的簡寫。
上面的定義符合函數符號直觀上的"唯一對應"。為了證明常數符號的"唯一性",需要以下元定理
元定理 —
說一階邏輯理論
L
{\displaystyle {\mathcal {L}}}
帶相等符號
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
,等同於要求:
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
除了變量
x
{\displaystyle x}
和
y
{\displaystyle y}
於
E
(
x
,
y
)
{\displaystyle {\mathcal {E}}(x,\,y)}
是完全自由外其他變量都完全被約束。
符合(E1)。
(E2) 對於任意變量
x
{\displaystyle x}
和
y
{\displaystyle y}
,若在公式
A
{\displaystyle {\mathcal {A}}}
中自由的
y
{\displaystyle y}
都不在
∀
x
{\displaystyle \forall x}
的範圍內。若以
A
y
{\displaystyle {\mathcal {A}}_{y}}
代表
A
{\displaystyle {\mathcal {A}}}
某些 自由的
x
{\displaystyle x}
被取代成
y
{\displaystyle y}
而成的新公式,則
⊢
L
E
(
x
,
y
)
⇒
(
A
⇒
A
y
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})}
證明
(
⇒
{\displaystyle \Rightarrow }
)
從(E1)+(E2')+(E2")+(E3)推出(E2)的過程分成幾個階段推廣(E2')
(1)含有常數符號的原子公式
取
c
j
{\displaystyle c_{j}}
為任意常數符號。目標是證明:對一段含常數符號
c
j
{\displaystyle c_{j}}
但不含任何函數符號的原子公式
B
(
x
,
x
,
c
j
)
{\displaystyle {\mathcal {B}}(x,\,x,\,c_{j})}
,若
B
(
x
,
y
,
c
j
)
{\displaystyle {\mathcal {B}}(x,\,y,\,c_{j})}
表
B
(
x
,
x
,
c
j
)
{\displaystyle {\mathcal {B}}(x,\,x,\,c_{j})}
裏某一個
x
{\displaystyle x}
被取代為
y
{\displaystyle y}
的新公式,則
⊢
L
E
(
x
,
y
)
⇒
[
B
(
x
,
x
,
c
j
)
⇒
B
(
x
,
y
,
c
j
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]}
(a)
(a)證明過程如下:
取一個不曾在
B
(
x
,
y
,
c
j
)
{\displaystyle {\mathcal {B}}(x,\,y,\,c_{j})}
出現的變量
z
{\displaystyle z}
。若以
B
(
x
,
x
,
z
)
{\displaystyle {\mathcal {B}}(x,\,x,\,z)}
表示
B
(
x
,
x
,
c
j
)
{\displaystyle {\mathcal {B}}(x,\,x,\,c_{j})}
內的
c
j
{\displaystyle c_{j}}
都 被取代成
z
{\displaystyle z}
的新公式,將之帶入 (E2')有
⊢
L
E
(
x
,
y
)
⇒
[
B
(
x
,
x
,
z
)
⇒
B
(
x
,
y
,
z
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]}
對上式,以變量
z
{\displaystyle z}
取(GEN)有
⊢
L
∀
z
{
E
(
x
,
y
)
⇒
[
B
(
x
,
x
,
z
)
⇒
B
(
x
,
y
,
z
)
]
}
{\displaystyle \vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}}
(b)
但從(A4)有
⊢
L
∀
z
{
E
(
x
,
y
)
⇒
[
B
(
x
,
x
,
z
)
⇒
B
(
x
,
y
,
z
)
]
}
⇒
{
E
(
x
,
y
)
⇒
[
B
(
x
,
x
,
c
j
)
⇒
B
(
x
,
y
,
c
j
)
]
}
{\displaystyle \vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}\Rightarrow \{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]\}}
這樣上式就可以與(b)式取MP,就會有(a)。
(2)含有任意項的原子公式
對一列項
T
1
,
⋯
,
T
m
{\displaystyle T_{1},\,\cdots ,\,T_{m}}
,若以
S
{\displaystyle S}
代表項
T
k
{\displaystyle T_{k}}
裏的一個
x
{\displaystyle x}
被取代成
y
{\displaystyle y}
而成的新項,那這樣可以用
A
j
m
(
T
1
,
⋯
,
S
,
⋯
,
T
m
)
{\displaystyle A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})}
代表
A
j
m
(
T
1
,
⋯
,
T
k
,
⋯
,
T
m
)
{\displaystyle A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})}
的
T
k
{\displaystyle T_{k}}
被取代成
S
{\displaystyle S}
所構成的新公式。那現在的目標是證明
⊢
L
E
(
x
,
y
)
⇒
[
A
j
m
(
T
1
,
⋯
,
T
k
,
⋯
,
T
m
)
⇒
A
j
m
(
T
1
,
⋯
,
S
,
⋯
,
T
m
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})\Rightarrow A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})]}
(c)
但根據(A4)和(GEN),只需要證明
⊢
L
E
(
x
,
y
)
⇒
[
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
T
k
,
x
k
+
1
,
⋯
,
x
m
)
⇒
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
S
,
x
k
+
1
,
⋯
,
x
m
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]}
(c')
就足夠了。更進一步的,由下面兩定理可以推出(c')
⊢
L
E
(
z
,
z
′
)
⇒
[
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
z
,
x
k
+
1
,
⋯
,
x
m
)
⇒
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
z
′
,
x
k
+
1
,
⋯
,
x
m
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(z,\,z^{\prime })\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z,\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z^{\prime },\,x_{k+1},\,\cdots ,\,x_{m})]}
(d)
⊢
L
E
(
x
,
y
)
⇒
E
(
T
k
,
S
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)}
(e)
也就是對(c)以變量
z
{\displaystyle z}
和
z
′
{\displaystyle z^{\prime }}
連續兩次使用(GEN),然後連續兩次與(A4)以MP律配合會得到
⊢
L
E
(
T
k
,
S
)
⇒
[
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
T
k
,
x
k
+
1
,
⋯
,
x
m
)
⇒
A
j
m
(
x
1
,
⋯
,
x
k
−
1
,
S
,
x
k
+
1
,
⋯
,
x
m
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(T_{k},\,S)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]}
然後將上式與(e)帶入(D1)就有(c')。但事實上(d)就是(E2')的特殊狀況,所以接下來只需要從(E2")證明(e),為此根據項的遞歸定義,以對項
T
k
{\displaystyle T_{k}}
裏有的函數符號數量做歸納:
函數符號數量為零的時候,(e)有兩種狀況(其中
c
j
{\displaystyle c_{j}}
為任意常數符號)
⊢
L
E
(
x
,
y
)
⇒
E
(
x
,
y
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(x,\,y)}
(e0)
⊢
L
E
(
x
,
y
)
⇒
E
(
c
j
,
c
j
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(c_{j},\,c_{j})}
(e0')
(e0)就只是(I)故顯然成立;另一方面,對(E1)使用(GEN)然後與(A4)配合就會有
⊢
L
E
(
c
j
,
c
j
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(c_{j},\,c_{j})}
故與(A1)配合就會有(e0'),至此函數符號數量為零情況的(e)已被證明。
若
T
k
{\displaystyle T_{k}}
內函數符號數量為
l
{\displaystyle l}
個,事實上會有一列函數符號數量小於
l
{\displaystyle l}
的項
S
1
,
⋯
,
S
n
{\displaystyle S_{1},\,\cdots ,\,S_{n}}
,而有
T
k
:
f
i
n
(
S
1
,
⋯
,
S
n
)
{\displaystyle T_{k}:f_{i}^{n}(S_{1},\,\cdots ,\,S_{n})}
若以
S
r
′
{\displaystyle {S_{r}}^{\prime }}
代表
S
r
{\displaystyle S_{r}}
中的某個
x
{\displaystyle x}
被取代成
y
{\displaystyle y}
而成的新項,那這就是
T
k
{\displaystyle T_{k}}
取代成新項
S
{\displaystyle S}
的詳細過程,那歸納法的前提就是
⊢
L
E
(
x
,
y
)
⇒
E
(
S
r
,
S
r
′
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })}
那對(E2")使用
n
{\displaystyle n}
次(GEN),然後同樣與(A4)以MP律配合
n
{\displaystyle n}
次有
⊢
L
E
(
S
r
,
S
r
′
)
⇒
E
[
f
i
n
(
S
1
,
⋯
,
S
r
,
⋯
,
S
n
)
,
f
i
n
(
S
1
,
⋯
,
S
r
′
,
⋯
,
S
n
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}[f_{i}^{n}(S_{1},\,\cdots ,\,S_{r},\,\cdots ,\,S_{n}),\,f_{i}^{n}(S_{1},\,\cdots ,\,{S_{r}}^{\prime },\,\cdots ,\,S_{n})]}
也就是
⊢
L
E
(
S
r
,
S
r
′
)
⇒
E
(
T
k
,
S
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}(T_{k},\,S)}
故將上式與歸納前提套入(D1)就會有
⊢
L
E
(
x
,
y
)
⇒
E
(
T
k
,
S
)
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)}
至此(e)已被歸納法證明。
(3)任意的公式
為了將(E2')從任意原子公式推廣到任意公式,根據語法對公式的遞歸定義,要分別對公式裏的量詞和邏輯連接詞的數量做歸納。
假設
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
為不含邏輯連接詞的任意公式:
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
沒有量詞的情況就只是(c)而已,故成立。
若假設對於量詞數量為
l
{\displaystyle l}
的
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
有(
B
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)}
代表
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
內某個自由的
x
{\displaystyle x}
被取代成
y
{\displaystyle y}
所成的新公式)
⊢
L
E
(
x
,
y
)
⇒
[
B
(
x
,
x
)
⇒
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]}
首先注意到新增量詞的時候,不可以取
∀
x
{\displaystyle \forall x}
或是
∀
y
{\displaystyle \forall y}
,否則上面的自由取代就會完全被破壞。故取個不是
x
{\displaystyle x}
也不是
y
{\displaystyle y}
的任意變量
z
{\displaystyle z}
,對上式使用(GEN),然後與(A6)、(A5)配合使用MP律有
⊢
L
E
(
x
,
y
)
⇒
[
∀
z
B
(
x
,
x
)
⇒
∀
z
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\forall z{\mathcal {B}}(x,\,x)\Rightarrow \forall z{\mathcal {B}}(x,\,y)]}
上式也就是量詞數量為
l
+
1
{\displaystyle l+1}
的狀況,而把(E2')推廣到了不含邏輯連接詞的任意公式上。
接下來對不含「
⇒
{\displaystyle \Rightarrow }
」的任意公式裏的「
¬
{\displaystyle \neg }
」的數量做歸納:
「
¬
{\displaystyle \neg }
」的數量為零的情況剛剛已經證明,不再贅述。
假設「
¬
{\displaystyle \neg }
」的數量為
l
{\displaystyle l}
,沒有「
⇒
{\displaystyle \Rightarrow }
」的公式下(E2')都對,那對「
¬
{\displaystyle \neg }
」的數量為
l
{\displaystyle l}
的
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
有(特別注意到推廣的(E2')也可以將
B
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)}
裏唯一的
y
{\displaystyle y}
取代成
x
{\displaystyle x}
)
⊢
L
E
(
y
,
x
)
⇒
[
B
(
x
,
y
)
⇒
B
(
x
,
x
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(y,\,x)\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]}
(f)
那根據(T)有
⊢
L
[
B
(
x
,
y
)
⇒
B
(
x
,
x
)
]
⇒
[
¬
B
(
x
,
x
)
⇒
¬
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}[{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]}
(g)
這樣對(f)和(g)套用(D1),結果再和(E3)套用(D1)一次就有
⊢
L
E
(
x
,
y
)
⇒
[
¬
B
(
x
,
x
)
⇒
¬
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]}
(f)
上式也就「
¬
{\displaystyle \neg }
」的數量為
l
+
1
{\displaystyle l+1}
的情況,故把(E2')推廣到了僅不含「
⇒
{\displaystyle \Rightarrow }
」的任意公式上。
為了要推廣到任意的公式上,我要要對「
⇒
{\displaystyle \Rightarrow }
」的數量做歸納:
「
⇒
{\displaystyle \Rightarrow }
」的數量為零的情況剛剛已經證明,不再贅述。
假設「
⇒
{\displaystyle \Rightarrow }
」的數量小於
l
{\displaystyle l}
的公式下(E2')都對,那對但數量合起來為
l
{\displaystyle l}
的
B
(
x
,
x
)
{\displaystyle {\mathcal {B}}(x,\,x)}
與
C
(
x
,
x
)
{\displaystyle {\mathcal {C}}(x,\,x)}
就會滿足
⊢
L
E
(
x
,
y
)
⇒
[
B
(
x
,
x
)
⇒
B
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]}
(*)
⊢
L
E
(
x
,
y
)
⇒
[
C
(
x
,
x
)
⇒
C
(
x
,
y
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]}
(**)
考慮到(D1)有
B
(
x
,
x
)
⇒
C
(
x
,
x
)
,
C
(
x
,
x
)
⇒
C
(
x
,
y
)
⊢
L
B
(
x
,
x
)
⇒
C
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x),\,{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)}
B
(
x
,
y
)
⇒
B
(
x
,
x
)
,
B
(
x
,
x
)
⇒
C
(
x
,
x
)
⊢
L
B
(
x
,
x
)
⇒
C
(
x
,
y
)
{\displaystyle {\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x),\,{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)}
那配上(*)與(**)就有
⊢
L
E
(
x
,
y
)
⇒
{
[
B
(
x
,
x
)
⇒
C
(
x
,
x
)
]
⇒
[
B
(
x
,
x
)
⇒
C
(
x
,
y
)
]
}
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]\}}
⊢
L
E
(
x
,
y
)
⇒
{
[
B
(
x
,
x
)
⇒
C
(
x
,
x
)
]
⇒
[
B
(
x
,
y
)
⇒
C
(
x
,
x
)
]
}
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {C}}(x,\,x)]\}}
上兩式就是所有「
⇒
{\displaystyle \Rightarrow }
」的數量為
l
+
1
{\displaystyle l+1}
的情況,故把(E2')推廣到了任意公式。
最後,取代
n
+
1
{\displaystyle n+1}
個
x
{\displaystyle x}
的狀況,就是取代
n
{\displaystyle n}
後再取代一次。所以可以由歸納法,從推廣後的(E2')推出(E2)
(
⇐
{\displaystyle \Leftarrow }
)
首先(E2')顯然只是(E2)的特例;要得到(E2")只要注意到由(E2)有
⊢
L
E
(
x
k
,
y
)
⇒
{
E
[
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
,
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
]
⇒
E
[
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
,
f
i
n
(
x
1
,
⋯
,
y
,
⋯
,
x
n
)
]
}
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow \{{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]\}}
然後對(E1)使用(GEN)再配合(A4)使用MP律有
⊢
L
E
[
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
,
f
i
n
(
x
1
,
⋯
,
x
k
,
⋯
,
x
n
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]}
所以對上面兩式套用(D2)就有(E2")。
至於(E3),注意到由(E2)有
⊢
L
E
(
x
,
y
)
⇒
[
E
(
x
,
x
)
⇒
E
(
y
,
x
)
]
{\displaystyle \vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {E}}(x,\,x)\Rightarrow {\mathcal {E}}(y,\,x)]}
那這樣對上式和(E1)套用(D2)就有(E3)
從上面可以得知,如果等式符號僅僅為斷言符號,那等式和它的公理 一節的等式公理模式 ,是等價於本節的(E1)+(E2')+(E2")。
由上面的元定理,對帶有等式符號的
L
{\displaystyle {\mathcal {L}}}
可以證明以下的等式性質
對任意常數符號
c
{\displaystyle c}
,上列元定理確保了
⊢
L
(
c
=
c
)
{\displaystyle \vdash _{\mathcal {L}}(c=c)}
(
x
=
c
)
,
(
y
=
c
)
⊢
L
(
x
=
y
)
{\displaystyle (x=c),\,(y=c)\vdash _{\mathcal {L}}(x=y)}
也就是常數符號的"唯一性"。
數學討論中,常常唯一存在某個符合特定條件的數,像是「存在唯一的實數
s
∈
R
{\displaystyle s\in \mathbb {R} }
使的對所有的實數
r
∈
R
{\displaystyle r\in \mathbb {R} }
,
r
+
s
=
r
{\displaystyle r+s=r}
」;更精確地來說,這句話的意思是:
「存在
s
∈
R
{\displaystyle s\in \mathbb {R} }
使的對所有的實數
r
∈
R
{\displaystyle r\in \mathbb {R} }
,
r
+
s
=
r
{\displaystyle r+s=r}
」且「對所有的
s
′
,
s
∈
R
{\displaystyle s^{\prime },\,s\in \mathbb {R} }
和所有
r
∈
R
{\displaystyle r\in \mathbb {R} }
,若
r
+
s
=
r
{\displaystyle r+s=r}
且
r
+
s
′
=
r
{\displaystyle r+s^{\prime }=r}
則
s
=
s
′
{\displaystyle s=s^{\prime }}
」
這樣一般來說,可以對任意變量
x
{\displaystyle x}
和合式公式
B
(
x
)
{\displaystyle {\mathcal {B}}(x)}
做以下的符號定義:
注意到要能定義唯一性,一階邏輯理論一定要帶有等號 。
上節所提到的例子,實際上就是所謂的實數
0
{\displaystyle 0}
,但常數符號不能憑空從理論中冒出來,所以仔細來說,「定義實數
0
{\displaystyle 0}
」的過程應該是在原來的理論添加新的常數符號「
0
{\displaystyle 0}
」與以下的公理:
「對所有的實數
r
∈
R
{\displaystyle r\in \mathbb {R} }
有
r
+
0
=
r
{\displaystyle r+0=r}
」
這樣的話,「
r
>
0
{\displaystyle r>0}
」就是一條含有新常數符號的敘述,它應等價於:
存在
s
∈
R
{\displaystyle s\in \mathbb {R} }
使「
r
>
s
{\displaystyle r>s}
且對所有的
x
∈
R
{\displaystyle x\in \mathbb {R} }
,
x
+
s
=
x
{\displaystyle x+s=x}
」
也就是說,添加「
0
{\displaystyle 0}
」創造了一套新理論,新理論的每條新敘述會對應到舊理論的某條舊敘述,且照理來說,新的對舊的也會對,反之亦然。
更一般的來說,如果新的一階邏輯理論,是在舊的理論增添一些新符號跟新公理(並額外要求新符號與舊公理相容 ),那為了讓新舊理論等效,對於任意新理論的合式公式
C
{\displaystyle {\mathcal {C}}}
,都要有某條相應的舊理論公式
C
′
{\displaystyle {\mathcal {C}}^{\prime }}
滿足以下條件[ 5] :
從條件(2)事實上就可以推出「若
⊢
o
C
′
{\displaystyle \vdash _{o}{\mathcal {C}}^{\prime }}
,則有
⊢
n
C
{\displaystyle \vdash _{n}{\mathcal {C}}}
」,因為
⊢
o
C
′
{\displaystyle \vdash _{o}{\mathcal {C}}^{\prime }}
的話, 新理論只是擴張舊理論而沒改變舊理論原生的定理,所以有
⊢
n
C
′
{\displaystyle \vdash _{n}{\mathcal {C}}^{\prime }}
,但這樣根據條件(2)跟MP律 就會有
⊢
n
C
{\displaystyle \vdash _{n}{\mathcal {C}}}
。所以條件(2)事實上是比「舊的對那新的也對」強的條件,但在之後的推導上(2)會比較方便。
在以嚴謹的方式實踐以上提及的直觀動機前,需要一個預備定理
證明
(
⇒
{\displaystyle \Rightarrow }
)
∃
!
B
(
x
)
⊢
(
∃
x
)
[
B
(
x
)
∧
C
(
x
)
]
⇒
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
{\displaystyle \exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Rightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]}
以下取一個不曾出現的變量
y
{\displaystyle y}
展開唯一性的定義
(1)
(
∀
x
)
(
∀
y
)
[
B
(
x
)
∧
B
(
y
)
⇒
(
x
=
y
)
]
{\displaystyle (\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]}
(Hyp)
(2)
B
(
y
)
{\displaystyle {\mathcal {B}}(y)}
(Hyp)
(3)
B
(
x
)
∧
C
(
x
)
{\displaystyle {\mathcal {B}}(x)\wedge {\mathcal {C}}(x)}
(Hyp)
(4)
B
(
x
)
∧
B
(
y
)
⇒
(
x
=
y
)
{\displaystyle {\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)}
(MP with A4, 1)
(5)
B
(
x
)
{\displaystyle {\mathcal {B}}(x)}
(MP with AND, 3)
(6)
B
(
x
)
∧
B
(
y
)
{\displaystyle {\mathcal {B}}(x)\wedge {\mathcal {B}}(y)}
(MP twice with AND, 2, 5)
(7)
(
x
=
y
)
{\displaystyle (x=y)}
(MP with 4, 6)
(8)
(
x
=
y
)
⇒
[
C
(
x
)
⇒
C
(
y
)
]
{\displaystyle (x=y)\Rightarrow [\,{\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)\,]}
(E2)
(9)
C
(
x
)
⇒
C
(
y
)
{\displaystyle {\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)}
(MP with 7, 8)
(10)
C
(
x
)
{\displaystyle {\mathcal {C}}(x)}
(MP with AND, 3)
(11)
C
(
y
)
{\displaystyle {\mathcal {C}}(y)}
(MP with 9, 10)
這樣根據(AND)和 (D1) 有
∃
x
!
B
(
x
)
,
B
(
y
)
,
B
(
x
)
∧
C
(
x
)
⊢
C
(
y
)
{\displaystyle \exists x!{\mathcal {B}}(x),\,{\mathcal {B}}(y),\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,\vdash \,{\mathcal {C}}(y)}
那這樣先使用(D)把
B
(
y
)
{\displaystyle {\mathcal {B}}(y)}
移到左邊,並對變量
x
{\displaystyle x}
使用(GENe)有
∃
x
!
B
(
x
)
,
∃
x
[
B
(
x
)
∧
C
(
x
)
]
⊢
B
(
y
)
⇒
C
(
y
)
{\displaystyle \exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)}
那這樣再對變量
y
{\displaystyle y}
使用(GEN)有
∃
x
!
B
(
x
)
,
∃
x
[
B
(
x
)
∧
C
(
x
)
]
⊢
∃
y
[
B
(
y
)
⇒
C
(
y
)
]
{\displaystyle \exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists y[\,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)\,]}
再使用(A4)把右側的變量
y
{\displaystyle y}
替換成
x
{\displaystyle x}
,再對
x
{\displaystyle x}
使用(GEN)有
∃
x
!
B
(
x
)
,
∃
x
[
B
(
x
)
∧
C
(
x
)
]
⊢
∃
x
[
B
(
x
)
⇒
C
(
x
)
]
{\displaystyle \exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists x[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]}
所以根據(D),本部分得証。
(
⇐
{\displaystyle \Leftarrow }
)
∃
!
B
(
x
)
⊢
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
⇒
(
∃
x
)
[
B
(
x
)
∧
C
(
x
)
]
{\displaystyle \exists !{\mathcal {B}}(x)\vdash (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]\Rightarrow (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]}
(1)
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
{\displaystyle (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]}
(Hyp)
(2)
B
(
x
)
{\displaystyle {\mathcal {B}}(x)}
(Hyp)
(3)
B
(
x
)
⇒
C
(
x
)
{\displaystyle {\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)}
(MP with A4, 1)
(4)
C
(
x
)
{\displaystyle {\mathcal {C}}(x)}
(MP with 2, 3)
(4)
B
(
x
)
∧
C
(
x
)
{\displaystyle {\mathcal {B}}(x)\wedge {\mathcal {C}}(x)}
(MP twice with AND, 2, 4)
也就是說
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
,
B
(
x
)
⊢
B
(
x
)
∧
C
(
x
)
{\displaystyle (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,{\mathcal {B}}(x)\,\vdash \,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)}
對變量
x
{\displaystyle x}
使用(GENe)有
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
,
∃
x
B
(
x
)
⊢
∃
x
[
B
(
x
)
∧
C
(
x
)
]
{\displaystyle (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]}
這樣根據(AND)和 (D1) 有
(
∀
x
)
[
B
(
x
)
⇒
C
(
x
)
]
,
∃
!
x
B
(
x
)
⊢
∃
x
[
B
(
x
)
∧
C
(
x
)
]
{\displaystyle (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists !x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]}
所以根據(D),本部分得証。
一般來說,如果變量
t
1
,
t
2
,
…
,
t
n
,
x
{\displaystyle t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x}
在
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)}
完全自由,且舊理論裏有:
(
U
{\displaystyle U}
)
⊢
o
∃
!
x
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle \vdash _{o}\exists !x{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)}
那所謂的新理論,就是添加一個函數符號
f
k
n
{\displaystyle f_{k}^{n}}
和以下的新公理:
(
U
′
{\displaystyle U^{\prime }}
)
B
[
t
1
,
t
2
,
…
,
t
n
,
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
{\displaystyle {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]}
如果僅僅是:
⊢
o
∃
!
x
B
(
x
)
{\displaystyle \vdash _{o}\exists !x{\mathcal {B}}(x)}
的話,添加的是常數符號
c
k
{\displaystyle c_{k}}
與以下的新公理:
(
U
{\displaystyle U}
)
B
(
c
k
)
{\displaystyle {\mathcal {B}}(c_{k})}
添加常數符號的情況可視為添加函數符號情況的特例,因為常數符號可以視為「零變量」的函數符號。
但不管如何,還需假設
f
k
n
{\displaystyle f_{k}^{n}}
和新理論的邏輯公理、量詞公理相容,也就是所有公理模式須涵蓋內含
f
k
n
{\displaystyle f_{k}^{n}}
的項 。特別像是(A4)這種將自由變量代換成項的公理模式,也就是說,若項
T
{\displaystyle T}
內含
f
k
n
{\displaystyle f_{k}^{n}}
,且公式
D
(
x
)
{\displaystyle {\mathcal {D}}(x)}
內自由的
x
{\displaystyle x}
都不在
T
{\displaystyle T}
的變量的量詞範圍內,那
∀
x
D
(
x
)
⇒
D
(
T
)
{\displaystyle \forall x{\mathcal {D}}(x)\Rightarrow {\mathcal {D}}(T)}
仍然是新理論的公理。
另外還需要考慮到
f
k
n
{\displaystyle f_{k}^{n}}
與等號的相容性(換句話說,新理論仍須是帶等號的一階邏輯理論),這樣的話,考慮到上面等式定理 所述的條件(E2''),需額外假設:
新理論的額外假設 —
對任何介於
1
{\displaystyle 1}
與
n
{\displaystyle n}
的下標
k
{\displaystyle k}
和變量
t
1
,
t
2
,
…
,
t
n
,
x
{\displaystyle t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x}
(
t
k
=
x
)
⇒
[
f
k
n
(
t
1
,
…
,
t
k
,
…
,
t
n
)
=
f
k
n
(
t
1
,
…
,
x
,
…
,
t
n
)
]
{\displaystyle (t_{k}=x)\Rightarrow [\,f_{k}^{n}(t_{1},\,\ldots ,\,t_{k},\,\ldots ,\,t_{n})=f_{k}^{n}(t_{1},\,\ldots ,\,x,\,\ldots ,\,t_{n})\,]}
是公理
(若是添加常數符號的特例,就不須額外假設以上的公理)
這樣就有以下直觀的定理
元定理 —
對變量
t
1
,
t
2
,
…
,
t
n
,
x
{\displaystyle t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x}
有
(E)
⊢
n
[
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
⇔
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle \vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Leftrightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)}
證明
(
⇒
{\displaystyle \Rightarrow }
)
⊢
n
[
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
⇒
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle \vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)}
(1)
(
y
=
x
)
⇒
[
B
(
t
1
,
t
2
,
…
,
t
n
,
y
)
⇒
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
]
{\displaystyle (y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,]}
(E2)
(2)
(
∀
y
)
{
(
y
=
x
)
⇒
[
B
(
t
1
,
t
2
,
…
,
t
n
,
y
)
⇒
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
]
}
{\displaystyle (\forall y)\{(y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\,]\}}
(GEN with 1,
y
{\displaystyle y}
)
(3)
[
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
=
x
]
⇒
{
B
[
t
1
,
t
2
,
…
,
t
n
,
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
⇒
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
}
{\displaystyle [\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow \{\,{\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,\}}
(MP with A4, 2)
(4)
[
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
=
x
]
⇒
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle [\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)}
(D2 with
U
′
{\displaystyle U^{\prime }}
, 3)
(
⇐
{\displaystyle \Leftarrow }
)
⊢
n
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
⇒
[
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
{\displaystyle \vdash _{n}{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]}
(1)
∀
x
∀
y
{
[
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
∧
B
(
t
1
,
t
2
,
…
,
t
n
,
y
)
]
⇒
(
x
=
y
)
}
{\displaystyle \forall x\forall y\{\,[\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\,]\Rightarrow (x=y)\,\}}
(MP with AND and
U
{\displaystyle U}
)
(2)
∀
x
{
{
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
∧
B
[
t
1
,
t
2
,
…
,
t
n
,
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
}
⇒
[
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
}
{\displaystyle \forall x{\big \{}\,\{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,{\big \}}}
(A4 with 1 and
y
{\displaystyle y}
)
(3)
{
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
∧
B
[
t
1
,
t
2
,
…
,
t
n
,
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
}
⇒
[
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
{\displaystyle \{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]}
(A4 with 2 and
x
{\displaystyle x}
)
(4)
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
{\displaystyle {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)}
(Hyp)
(5)
B
(
t
1
,
t
2
,
…
,
t
n
,
x
)
∧
B
[
t
1
,
t
2
,
…
,
t
n
,
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
]
{\displaystyle {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]}
(AND with
U
{\displaystyle U}
and 4)
(6)
x
=
f
k
n
(
t
1
,
t
2
,
…
,
t
n
)
{\displaystyle x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})}
(MP with 3 and 5)
換句話說,「
s
=
0
{\displaystyle s=0}
」在新理論裏等價於 「對所有的實數
r
∈
R
{\displaystyle r\in \mathbb {R} }
,
r
+
s
=
r
{\displaystyle r+s=r}
」。
下面列出了一些重要的元邏輯定理。
不像命題演算 ,一階邏輯是不可判定性的。對於任意的公式P,可以證實沒有判定過程 ,判定P是否有效,(參見停機問題 )。(結論獨立的來自於邱奇 和圖靈 。)
有效性 的判定問題是半可判定的。按哥德爾完備性定理 所展示的,對於任何有效的 公式P, P是可證明的。
一元斷言邏輯 (就是說,斷言只有一個參數的斷言邏輯)是可判定的。
用自然語言表達的概念必須在一階邏輯(FOL)可以為為其效力之前必須被轉換到FOL,而在這種轉換中可能有一些潛在的缺陷。在FOL中,
p
∨
q
{\displaystyle p\lor q}
意味着「要麼p要麼q要麼二者」,就是說它是「包容性」的。在英語中,單詞「or」有時是包容性的(比如,「加牛奶或糖?」),有時是排斥性的(比如,「喝咖啡或茶?」,通常意味着取其中一個或另一個但非二者)。類似的,英語單詞「some」可以意味着「至少一個,可能全部」,有時意味着「不是全部,可能沒有」。英語單詞「and」有時要按「or」轉換(比如,「男人和女人可以申請」)。
[ 6]
所有數學概念都有它的強項和弱點;下面列出一階邏輯的一些問題。
帶有等式的FOL不包含或允許定義if-then-else斷言或函數if(c,a,b),這裏的c是表達為公式的條件,而a和b是要麼都是項要麼都是公式,並且它的結果是a如果c為真,或者b如果它為假。問題在於FOL中,斷言和函數二者只接受(「非布林類型」)項作為參數,而條件的明確表達是(「布林類型」)公式。這是不幸的,因為很多數學函數是依據if-then-else而方便的表達的,而if-then-else是描述大多數電腦程式的基礎。
在數學上,有可能重定義匹配公式算子的新函數的完備集合,但是這是非常笨拙的。[ 7]
斷言if(c,a,b)如果重寫為
(
c
∧
a
)
∨
(
¬
c
∧
b
)
{\displaystyle (c\wedge a)\lor (\neg c\wedge b)}
就可以在FOL中表達,但是如果條件c是複雜的這就是笨拙的。很多人擴充FOL增加特殊情況斷言叫做「if(條件,a, b)」(這裏a和b是公式)和/或函數「ite(條件,a, b)」(這裏的a和b是項),它們都接受一個公式作為條件,並且等於a如果條件為真,或b如果條件為假。這些擴充使FOL易於用於某些問題,並使某類自動定理證明更容易。[ 8]
其他人進一步擴充FOL使得函數和斷言可以在任何位置接受項和公式二者。
除了在公式(「布林類型」)和項(「非布林類型」)之間的區別之外,FOL不包括類型(種類)到自身的概念中。
某些人爭辯說缺乏類型是巨大優點
[ 9] ,而很多其他人發覺了定義和使用類型(種類)的優點,比如幫助拒絕某些錯誤或不想要的規定
[ 10] 。
想要指示類型的那些人必須使用在FOL中可獲得的符號來提供這種資訊。這麼做使得這種表達更加複雜,並也容易導致錯誤。
單一參數斷言可以用來在合適的地方實現類型的概念。例如:
∀
x
(
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
)
{\displaystyle \forall x(Man(x)\rightarrow Mortal(x))}
,
斷言Man(x)可以被認為是一類「類型斷言」(就是說,x必須是男人)。
斷言還可以同指示類型的「存在」量詞一起使用,但這通常應當轉而與邏輯合取算子一起來做,比如:
∃
x
(
M
a
n
(
x
)
∧
M
o
r
t
a
l
(
x
)
)
{\displaystyle \exists x(Man(x)\wedge Mortal(x))}
(「存在既是男人又是人類的事物」)。
容易寫成
∃
x
M
a
n
(
x
)
→
M
o
r
t
a
l
(
x
)
{\displaystyle \exists xMan(x)\rightarrow Mortal(x)}
,但這將等價與
∃
x
¬
M
a
n
(
x
)
∨
∃
x
M
o
r
t
a
l
(
x
)
{\displaystyle \exists x\neg Man(x)\lor \exists xMortal(x)}
(「存在不是男人的事物或者存在是人類的事物」),這通常不是想要的。類似的,可以做一個類型是另一個類型的子類型的斷言,比如:
∀
x
(
M
a
n
(
x
)
→
M
a
m
m
a
l
(
x
)
)
{\displaystyle \forall x(Man(x)\rightarrow Mammal(x))}
(「對於所有x,如果x是男人,則x是哺乳動物)。
從Löwenheim–Skolem定理 得出在一階邏輯中不可能刻畫有限性或可數性。若一階理論有任意有限大的模型,則也有無窮大的模型,所以說不能刻劃有限性。[ 11] :1 而若理論有某個無窮基數大小的模型,則也必有任意更大的模型,所以不能刻劃可數性。[ 12] :45 另一個例子,是無法用一階語言將實數系 公理化,因為不論用何種一階理論描述,既然該理論有實數系此種無窮模型(大小為
2
ℵ
0
{\displaystyle 2^{\aleph _{0}}}
),所以必有比實數系更大(比如
2
2
ℵ
0
{\displaystyle 2^{2^{\aleph _{0}}}}
)的另一個模型,從而該理論不是(唯一地)刻劃實數系的性質。實數系滿足的公理中,有上確界 性質一項,它聲稱實數的所有有界的、非空集合都有上確界 。一階邏輯祗能對元素量化,但此公理中,要對模型的全部子集量化,這就需要二階邏輯 了。[ 13] :30
很多情況可以被建模為節點和有向連接(邊)的圖 。例如,效驗很多系統要求展示不能從「好」狀態觸及到「壞」狀態,而狀態的相互連接經常可以建模為圖。但是,可以證明這種可及性不能用斷言邏輯完全表達。換句話說,沒有斷言邏輯公式f,帶有u和v作為它的唯一自由變數,而R作為它唯一的(2元)斷言符號,使得f在一個有向圖中成立,如果在這個圖中存在從關聯於u的節點到關聯於v的節點的路徑。[ 14]
^ Mendelson, Elliott. Introduction to Mathematical Logic . Van Nostrand Reinhold. 1964: 56 .
^ Skolem's paradox and constructivism Charles McCarty & Neil Tennant
^ 3.0 3.1 Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.40 ISBN 978-1482237726
^ Elliott Mendelson. Introduction to Mathematical Logic - 6th Edition , p.29 ISBN 978-1482237726
^ 5.0 5.1 Stephen Cole Kleene Introduction to Metamathematics , p.405 ISBN 978-0923891572
^ Suber, Peter, Translation Tips , [2007-09-20 ] , (原始內容 存檔於2010-03-08)
^ Otter Example if.in , [2007-09-21 ] , (原始內容存檔 於2009-01-11)
^
Manna, Zohar, Mathematical Theory of Computation, McGraw-Hill Computer Science Series, New York, New York: McGraw-Hill Book Company: 77–147, 1974, ISBN 0-07-039910-7
^ Leslie Lamport, Lawrence C. Paulson.
Should Your Specification Language Be Typed?
ACM Transactions on Programming Languages and Systems.
1998.
http://citeseer.ist.psu.edu/71125.html (頁面存檔備份 ,存於互聯網檔案館 )
^ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html (頁面存檔備份 ,存於互聯網檔案館 )
^ Mahesh Viswanathan. Finite Model Theory (PDF) . [2021-11-14 ] . (原始內容 (PDF) 存檔於2021-07-13).
^ David Marker. Model Theory: An Introduction. Graduate Texts in Mathematics 217 . Springer. 2002.
^ Johnstone, P. T. Notes on logic and set theory . Cambridge University Press . 1987. doi:10.1017/CBO9781139172066 .
^
Huth, Michael; Ryan, Mark, Logic in Computer Science, 2nd edition: 138–139, 2004, ISBN 0-521-54310-X