一階邏輯的形式理論 可分成幾個部份:
語法 :決定哪些符號組合是合式公式 。(直觀上的“文法無誤的敘述”)
推理規則:由合式公式符號組合出新合式公式的規則(直觀上的“推理”)
公理:一套合式公式(直觀上的基本假設)
一套理論能容許多少符號,取決於人類根据物理定律 能塑造多少符號。但以目前無法確知宇宙是不是有限,或是是否可無限制分割。雖然所有的公理化集合論 都以量詞的形式隱晦的承認無窮的存在(如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] 會額外採用這個符號。 注意:並非所有的符號都是必需的。比如,在比較極端的情况中,因为謝費爾豎線 (或異或 )的布林代數 完備性使得所有不含量詞的邏輯公理都可以用謝費爾豎線表述,而大幅減少基礎的邏輯聯結詞。
另外,一些作者並沒有將語義學 和形式理論 劃分清楚,而會將真值常數納入符號的一環:用 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}
)以下面的規則遞迴地定義:
原子公式為公式。(美觀起見,在原子公式外面包一層括弧也是公式)
若
A
{\displaystyle {\mathcal {A}}}
為公式,則
(
¬
A
)
{\displaystyle (\neg {\mathcal {A}})}
為公式。
若
A
{\displaystyle {\mathcal {A}}}
與
B
{\displaystyle {\mathcal {B}}}
為公式,則
(
A
⇒
B
)
{\displaystyle ({\mathcal {A}}\Rightarrow {\mathcal {B}})}
為公式。
若
A
{\displaystyle {\mathcal {A}}}
為公式,
x
{\displaystyle x}
為任意變數,則
(
∀
x
A
)
{\displaystyle (\forall x{\mathcal {A}})}
為公式。 (美觀起見
(
∀
x
)
A
:=
∀
x
A
{\displaystyle (\forall x){\mathcal {A}}:=\forall x{\mathcal {A}}}
,也就是裡面的量詞有無外包括弧都是公式)
合式公式只能通过以上四點,於有限步驟內建構出來。
另外成對的中括弧跟大括弧,符號辨識上視為成對的小括弧,而草書的大寫西方字母 為公式的代號。
舉例來說,
{
(
∀
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}
(邏輯連結詞的符號轉換)
對於公式
A
{\displaystyle {\mathcal {A}}}
和
B
{\displaystyle {\mathcal {B}}}
:
A
⇒
B
{\displaystyle {\mathcal {A}}\Rightarrow {\mathcal {B}}}
和
A
{\displaystyle {\mathcal {A}}}
組合出
B
{\displaystyle {\mathcal {B}}}
。直觀意義非常明顯,就是p =>q 且p 可以推出q 。
它们实际上是公理模式 ,代表著“跟自然數一樣多”條的公理。
以下的
x
{\displaystyle x}
為任意變數,
B
{\displaystyle {\mathcal {B}}}
、
C
{\displaystyle {\mathcal {C}}}
為任意公式。
(A4)
T
{\displaystyle T}
是一個項,
t
{\displaystyle t}
為
T
{\displaystyle T}
中出現的任意變數;若
B
{\displaystyle {\mathcal {B}}}
裡,所有
∀
t
{\displaystyle \forall t}
的的範圍裡都沒有自由的
x
{\displaystyle x}
(這個情況稱為
B
{\displaystyle {\mathcal {B}}}
裡項
T
{\displaystyle T}
對
x
{\displaystyle x}
是自由的),則
[
(
∀
x
)
B
(
x
)
]
⇒
[
B
(
T
)
]
{\displaystyle [(\forall x){\mathcal {B}}(x)]\Rightarrow [{\mathcal {B}}(T)]}
為公理
其中
B
(
T
)
{\displaystyle {\mathcal {B}}(T)}
代表把
B
{\displaystyle {\mathcal {B}}}
裡自由的
x
{\displaystyle x}
都取代為
T
{\displaystyle T}
所得到的新公式。 (A5)如果
x
{\displaystyle x}
在
B
{\displaystyle {\mathcal {B}}}
裡完全被約束,則
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
B
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [{\mathcal {B}}\Rightarrow (\forall x{\mathcal {C}})]}
為公理 (A6)
[
(
∀
x
)
(
B
⇒
C
)
]
⇒
[
(
∀
x
B
)
⇒
(
∀
x
C
)
]
{\displaystyle [(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [(\forall x{\mathcal {B}})\Rightarrow (\forall x{\mathcal {C}})]}
為公理
(A7) 若
B
{\displaystyle {\mathcal {B}}}
是公理,
x
{\displaystyle x}
是任意變數,則
(
∀
x
)
B
{\displaystyle (\forall x){\mathcal {B}}}
也是公理。
它们实际上是公理模式 。
等式和它的公理 编辑
根據不同作者的看法,甚至是理論本身的需求,「等式」在形式理論裡可能是斷言符號或是一段公式(如 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}}
的取值換為論域的任意元素仍然為真)
更進一步的來說
在一套解釋
M
{\displaystyle M}
下,不管怎麼樣的變數取值,公式
B
{\displaystyle {\mathcal {B}}}
都為真,則稱為
M
{\displaystyle M}
下
B
{\displaystyle {\mathcal {B}}}
為真 ,以符號
M
⊨
B
{\displaystyle M\vDash {\mathcal {B}}}
簡記。若沒有變數取值可以滿足
B
{\displaystyle {\mathcal {B}}}
,則稱
M
{\displaystyle M}
下
B
{\displaystyle {\mathcal {B}}}
為假 。
若任意解釋下公式
B
{\displaystyle {\mathcal {B}}}
都為真,稱
B
{\displaystyle {\mathcal {B}}}
為邏輯有效的 (logically valid) (類似於命題邏輯 的恆真式 )
若一階邏輯理論
L
{\displaystyle {\mathcal {L}}}
的公理都於
M
{\displaystyle M}
為真,稱解釋
M
{\displaystyle M}
為
L
{\displaystyle {\mathcal {L}}}
之模型 (model)
代數化語義 编辑
另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數 擴展而成。有如下幾種類型:
這些代數 都是純粹擴展兩元素布林代數 而成的格 。
塔斯基和葛范德於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}}}
的證明:
C
1
{\displaystyle {\mathcal {C}}_{1}}
:
{
B
⇒
[
(
B
⇒
B
)
⇒
B
]
}
⇒
{
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
}
{\displaystyle \{{\mathcal {B}}\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\}\Rightarrow \{[{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})\}}
(公理A2)
C
2
{\displaystyle {\mathcal {C}}_{2}}
:
B
⇒
[
(
B
⇒
B
)
⇒
B
]
{\displaystyle {\mathcal {B}}\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]}
(公理A1)
C
3
{\displaystyle {\mathcal {C}}_{3}}
:
B
⇒
(
B
⇒
B
)
{\displaystyle {\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})}
(公理A1)
C
4
{\displaystyle {\mathcal {C}}_{4}}
:
[
B
⇒
(
B
⇒
B
)
]
⇒
(
B
⇒
B
)
{\displaystyle [{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})}
(
C
1
{\displaystyle {\mathcal {C}}_{1}}
和
C
2
{\displaystyle {\mathcal {C}}_{2}}
加上MP律)
C
5
{\displaystyle {\mathcal {C}}_{5}}
:
B
⇒
B
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {B}}}
(
C
4
{\displaystyle {\mathcal {C}}_{4}}
和
C
3
{\displaystyle {\mathcal {C}}_{3}}
加上MP律)
以上其實是蘊含了無限多定理的元定理 的證明(因為沒有給出合式公式的明確形式)。方便起見,這種元定理 還是會稱為定理並以同樣的形式來表達。
直觀上的證明,總是會有一些“前提假設”,對此,若以
Γ
{\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)會得出不但直觀且實用的演繹元定理 :
(D)Metatheorem of Deduction:
一階邏輯理論
L
{\displaystyle {\mathcal {L}}}
下,若有
Γ
,
B
⊢
L
C
{\displaystyle \Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}}
,則有
Γ
⊢
L
B
⇒
C
{\displaystyle \Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}}
因為
Γ
{\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)也會省略過程,單有結果和代號標註。
(DNe) Double negation, elimination
⊢
¬
¬
A
⇒
A
{\displaystyle \vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}}
證明
(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)
(DNi) Double negation, introduction
⊢
A
⇒
¬
¬
A
{\displaystyle \vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}}
證明
(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)
上面兩定理表達了雙否定推理上等價於於原公式,引用兩者任一會都以(DN)簡寫。
(T1) Transposition-1
¬
A
⇒
¬
B
⊢
B
⇒
A
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}}
證明
(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}}}
證明
(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)
以上二定理表說明
B
⇒
A
{\displaystyle {\mathcal {B}}\Rightarrow {\mathcal {A}}}
推理上等價於
¬
A
⇒
¬
B
{\displaystyle \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}}
,引用這兩個定理中任一都以(T)表示。
由(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}}}
證明提示 :仿(C1)。
以下為"且"的交換性
⊢
(
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}}}
證明提示 : (AND)
"或"也有類似的性質
(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}}}
證明提示 : (M1), (M2), (M3)
"且"和"或"之間還有分配律
(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)可以稍加修飾,以套用在含有存在量詞的公式上
元定理 (GENe):
若變數
x
{\displaystyle x}
在
Γ
{\displaystyle \Gamma }
的公式和
C
{\displaystyle {\mathcal {C}}}
裡都完全被約束則
(1) 若
Γ
⊢
A
⇒
B
{\displaystyle \Gamma \vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}}
則
Γ
⊢
(
∃
x
)
A
⇒
(
∃
x
)
B
{\displaystyle \Gamma \vdash (\exists x){\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}}
(2) 若
Γ
⊢
B
⇒
C
{\displaystyle \Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}}
則
Γ
⊢
(
∃
x
)
B
⇒
C
{\displaystyle \Gamma \vdash (\exists x){\mathcal {B}}\Rightarrow {\mathcal {C}}}
證明提示 :對(GEN)使用(T)和(A5)
量詞的可交換性 编辑
由普遍化,很容易證明以下關於"交換性"的定理
(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}