一阶逻辑
一阶逻辑 是使用於数学 、哲学 、语言学 及電腦科學 中的一种形式系统 ,也可以稱為:一阶斷言演算 、低階斷言演算 、量化理論 或谓词逻辑 。一階邏輯和命題邏輯 的不同之處在於,一階邏輯包含量詞 。
高階邏輯 和一階邏輯不同之處在於,高階邏輯的斷言符號可以有斷言符號或函數符號當做引數 ,且容許斷言量詞或函數量詞[ 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]
一阶逻辑的限制
所有数学概念都有它的强项和弱点;下面列出一阶逻辑的一些问题。
难于表达if-then-else
带有等式的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
来源
外部链接