owned this note
owned this note
Published
Linked with GitHub
# 一階邏輯
## 簡介
不同於命題邏輯,自一階邏輯,我們開始關心一段敘述如何組成。
從一般語言敘述的構成來看,如果我們不照慣例,而把所有的東西都說得清清楚楚的話,照理來說一段敘述應該是 "主詞+動詞+受詞"、"主詞+動詞"、"主詞+動詞謂語+修飾詞"的主要架構,配上動詞、主詞和受詞的修飾語或修飾子句構成的。但數學關心的,只是一個對象有怎麼樣的狀態,則另一個對象會有怎樣的狀態,也就是"主詞+動詞謂語+修飾詞"的架構配上推理的關係。描述狀態不外乎辨識特徵,事實上跟定義"集合"的本質,也就是辨別一個群體的共通性做的事是一樣的。
一段敘述都有它敘述的對象;比如說「業界(**有人**)對這個產品有興趣」、「(**所有**)外國旅客入境前都要防疫隔離」;邏輯學上,"**有人**"(更一般的說**存在一個人**)跟"**所有人**"(注意到所有外國旅客是**不是本國籍且身在我國**的所有人的略語)這兩個表述敘述對象範圍的詞語被稱為**量詞**(quantifier)。顯然外國的旅客不只一個,這就是需要在語意上說明描述範圍的**變數**(variable),也就是每個變數都有它的取值範圍。(外國旅客是從所有人類裡取值,找有外國國籍且身在我國的人類)
數理邏輯上,"所有的變數$\displaystyle x$的取值滿足合式公式$\mathcal{A}$"以$(\forall x)\mathcal{A}$代表;類似的"存在變數$\displaystyle x$的取值滿足合式公式$\mathcal{A}$"以$(\exists x)\mathcal{A}$代表,其實也就是$\neg(\forall x)(\neg\mathcal{A})$。類似的,$(\forall x)\mathcal{A}$就是$\neg(\exists x)(\neg\mathcal{A})$。
要構成一段敘述,我們還需要其他要素;比如說"這個產品"就是一個**常數**(constant);**有興趣**代表著一種人和產品之間的**關係**;類似的,外國旅客的"定義"是來自國家和入境旅客的國籍隸屬"關係"。在邏輯學上我們用**謂詞符號**(predicate letter)去形式的表示"關係"。
數理邏輯上,兩個變數$\displaystyle x$和$\displaystyle y$的謂詞符號通常會用$\displaystyle A_{i}^{2}(x,y)$代表;其中$\displaystyle i$提醒我們理論裡可能不只一種"關係",$\displaystyle 2$提醒我們是描述"兩者之間的關係",這是因為關係可以描述到兩者以上(比如說三維空間中某一點在某區域內,那這點的三個座標跟這個區域就有"隸屬"關係)。只有一個對象的"謂詞符號"可以代表隸屬於特定群體的關係(也就是固定群體變數的取值)
特別注意到$\displaystyle A_{i}^{2}(x,y)$跟$\displaystyle A_{i}^{2}(y,x)$是不一樣的東西,就好比如果甲是乙的父親的話,反過來乙並不一定是甲的父親;對某些關係來講擺放的變數順序是很重要的,但像是相等、朋友關係等等就不是重要的。
另日常生活中會提到「你的身分」或是「一對夫妻的第一個小孩」這種可以用關係描述的片語。但是這兩段片語有個共同的特徵;每個人只有一種身分;同樣每對夫妻也只有一個第一個小孩;與其描述隸屬"關係",我們反而對獨有的那個對應物更有興趣,一般來說,是**不同組變數的取值能對到的唯一值**(比如說加法的結果都只有一個),這在邏輯學上以**函數符號**(function letter)去形式的代表。
數理邏輯裡,一組變數$\displaystyle x_1,x_2,....,x_n$的一個函數符號是以$\displaystyle f_{i}^{n}(x_1,x_2,....,x_n)$代表。
當然一般的敘述還不只有這些,像是「(所有)親子關係都可以用核酸檢定法驗證」、「(所有)國家都應該保護它的僑民」這種對"關係"和"變數取值範圍"(甚至函數符號)使用量詞的敘述。邏輯學上有兩種不一樣的處理;第一種是把關係、變數取值範圍和函數符號都解釋為**集合**(為何如此很快下面"一階邏輯的語意"一節就會說明),也就是說,我們需要一個以集合為變數取值的形式理論,稱為**集合論**。另一種方法,是仿造日常語言,直觀的把量詞擴充到關係和函數符號甚至取值範圍,但是這種方法在語意的解釋上一樣需要集合論,而且語意跟形式理論的聯繫不是很好,所以第一種方法是大部分數學家常用的方法。雖然一套嚴謹的集合論是依賴於一套有量詞的形式理論,但我們仍然可以先非正式的討論量詞的語意,以此為動機選取邏輯公理。等到有正確的集合論以後,再回過頭來嚴謹討論一階邏輯的語意
量詞只能施用在變數上的形式理論被稱為**一階邏輯**(first-order logic),反之稱為**高階邏輯**(Higher-order logic)。
### 量詞
對於$(\forall y)\mathcal{B}$,我們稱$\mathcal{B}$是量詞$\forall y$的**範圍**(scope),如果變數$\displaystyle y$出現在量詞$\forall y$的範圍裡,我們稱此次出現的$\displaystyle y$是**被限制的**(bounded);反之稱為**自由的**(free)。在一段合式公式裡,同個變數可能在某個地方自由,但另一個地方是被限制的,如
: $\forall y[A^{2}_{1}(x,y)]\Rightarrow A^{1}_{1}(y)$
第一次出現的$\displaystyle y$是被限制的;但第二次出現是自由的。我們說$\displaystyle x$在一條合式公式裡都不自由的時候,**代表$\displaystyle x$每個地方都被限制,或更有可能是$\displaystyle x$根本沒出現過**。
$\displaystyle y$完全不在量詞$\forall y$的範圍時,$(\forall y)\mathcal{B}$跟$\mathcal{B}$在語意上等價。
### 項
很顯然一段"合法"的敘述,單有對象是沒有用的,比如說「醫生!」、「長孫!」、「獨子的身分!」都是一些語意隱晦的敘述。為了更清楚說明這一點,考慮到一般情況下,函數符號是可能被連續施用(比如說二次多項式就是加法跟乘法的連續施用結果),為此我們定一個新名詞,**項**(term):
:::success
$\displaystyle (1)$變數和常數都是項
$\displaystyle (2)f^{n}_{k}$是一個函數符號,$\displaystyle t_1,t_2,....,t_n$是項,則$\displaystyle f^{n}_{k}(t_1,t_2,....,t_n)$是項。
$\displaystyle (3)$項只能透過以上兩點建構出來。
:::
所謂的**原子公式**(atomic formula),也就是最基本的一段敘述,型如$\displaystyle A^{n}_{k}(t_1,t_2,....,t_n)$,其中$\displaystyle t_1,t_2,....,t_n$是一組項。也就是形如「醫生是(她的)長孫!」「獨子的身分是醫生!」。而合式公式就是以原子公式為基礎,配上命題連接詞跟量詞組合而成的!
## 一階邏輯的語意
本節的目的在於直觀的解釋新增公理的合理性,而不是給予一階邏輯的**語意**(semantics)一套嚴謹的理論。
雖然從動機上來講,我們需要小心地確認量詞於一般敘述的意義,由此才能設計出讓我們滿意的一階邏輯形式理論;但從推演的角度來講,一階邏輯的語意只是公理化集合論架構下的附屬品(實用角度來講,一種方便確定一段$\displaystyle wf$是不是定理的辦法),說直接一點,與下面將建構出來的形式理論相容的語意解釋不只有一種,就像**命題邏輯**的形式理論,並沒有禁止多值邏輯的語意詮釋。
### 解釋
要定義與甲的親子關係,事實上可以用列舉甲的所有兒女來定義。比較數學化的方式,就是用(甲,兒子1)、(甲,兒子2)、....、(甲,女兒1)、(甲,女兒2),....的方法;那全球(針對父親)的親子關係就可以寫成
(父親1,父親1的兒子1)、(父親1,父親1的兒子2)、....、(父親1,父親1的女兒1)、(父親1,父親1的女兒2)、....
(父親2,父親2的兒子1)、(父親2,父親2的兒子2)、....、(父親2,父親2的女兒1)、(父親2,父親2的女兒2)、....
. . . .
. . . .
. . . .
. . . .
所以說的一般一點,兩者之間的關係就是(x,y)這樣的二元有序對集合,只不過x和y的取值範圍都有限制;像是這個例子就是從"所有人類中取值",配成(人類A,人類B)這樣的有序對;但人類A必須都是男性且生過小孩;而且隨意把人類B配在有序對的第二個位置,不見得人類B就是人類A生的。當然除了笨拙地列舉去定義親子關係,我們可以用DNA定序、或是其他"比較聰明"的方法去定義,但這就是另外個故事了,牽涉到滿足一段敘述的所有值,怎麼組成一個集合;而滿足兩段不同敘述的兩個集合會不會相等的問題。以我們目前的能力還無法嚴謹的去討論。
所以關係是所有二元有序對(x,y)構成的集合的一部分(稱為子集合)。如果把所有變數取的值聚集起來,組成一個集合,寫成$\displaystyle D$,那我們用$\displaystyle D^2$代表所有可能取值的二元有序對所聚集而成的集合。
說的更一般,n個變數之間的關係就是$\displaystyle D^n$──也就是所有可能取值的n元有序對$\displaystyle(x_1, x_2, ...., x_n)$構成的集合──的子集合
同樣的道理,我們可以把n個數字的相加表達為$\displaystyle(x_1, x_2, ...., x_n, x_1+x_2+....+x_n)$這樣的關係,但從敘述的目的上,我們比較喜歡$D^n\to D$這樣的符號提醒自己這是一個對應,是從每個n元有序對對應到一個$\displaystyle D$裡的值(一個"夠廣大"的取值範圍要包括加法的結果!)。而更一般的來說,$\displaystyle f_{i}^{n}(x_1,x_2,....,x_n)$就是被解釋成$D^n\to D$這樣的對應。
如此一來我們就有一套解釋一階邏輯語意的要素:
:::success
一個一階邏輯的**解釋**(interpretation)$\displaystyle M$需要有以下的要素:
(1)**所有變數取值的範圍**,稱為**論域**(domain of discourse)。以$\displaystyle D$代表。
(2)謂詞符號$\displaystyle A_{i}^{n}$被解釋為某個$\displaystyle D^n$的子集合,以${(A_{i}^{n})}_{M}$代表
(3)函數符號$\displaystyle f_{i}^{n}$被解釋成某個從$D^n\to D$的對應規則(也就是函數),以${(f_{i}^{n})}_{M}$代表
(4)常數$\displaystyle a$被解釋成某個屬於$\displaystyle D$的固定值,以$\displaystyle a_M$代表
:::
接下來我們說明這些要素如何適當的解釋一階邏輯
### 變數的解釋
窮人類能力所及,我們最多可以討論跟自然數一樣多的變數$\displaystyle x_1, x_2, x_3,....$所以一組變數的取值,就是從$\displaystyle D$取出如$\displaystyle a_1, a_2, a_3,....$這樣的序列,以${\{a_i\in D\}}_{i\in\mathbb{N}}$簡記,
其中$i\in\mathbb{N}$的意思是$\displaystyle i$是自然數(也就是$\displaystyle i$在自然數集合$\mathbb{N}$裡),$a_i\in D$的意思就是第$\displaystyle i$個變數從$\displaystyle D$取的值是$\displaystyle a_i$。如果論域在上下文很明顯的話,我們會把變數取值簡記為${\{a_i\}}_{i\in\mathbb{N}}$。
(事實上序列是一個由$\mathbb{N}$到$\displaystyle D$的對應,所以序列也是一個函數;所以也是一個關係,從而更能看成一個二元有序對的集合)
### 項的解釋
:::success
所有變數的取值是${\{a_i\}}_{i\in\mathbb{N}}$,在這種情況下項在$\displaystyle D$的對應值如下
(1)變數$\displaystyle x_j$的對應值是$\displaystyle a_j$;常數$\displaystyle a$的對應值是$\displaystyle a_M$
(2)在變數取值${\{a_i\}}_{i\in\mathbb{N}}$下,項$\displaystyle t_1, t_2,....,t_n$的對應值分別是$\displaystyle (t_1)_M, (t_2)_M, ...., (t_n)_M$,那$\displaystyle f^{n}_{k}(t_1,t_2,....,t_n)$在${\{a_i\}}_{i\in\mathbb{N}}$下的對應值是
: $\displaystyle {(f^{n}_{k})}_M[(t_1)_M, (t_2)_M, ...., (t_n)_M]$
:::
注意$\displaystyle f(a_1, a_2,....,a_n)$代表依照**函數]]$\displaystyle f$的對應規則下n元有序對$\displaystyle (a_1, a_2,....,a_n)$所對應的函數值。直觀來說,就是輸入了n個變數值所得出的"輸出值"。一個最簡單的輸出規則,就是輸入$\displaystyle (a_1, a_2,....,a_n)$會輸出$\displaystyle a_j$(也就是俗稱的第$\displaystyle j$個分量)
### 邏輯符號的解釋
事實上一階邏輯的合式公式規則,只是多要求:
: *原子公式是$\displaystyle wf$
: *$\mathcal{B}$是$\displaystyle wf$,則$(\forall x_i)\mathcal{B}$也是$\displaystyle wf$
如此一來,我們可以依照合式公式規則給所有的$\displaystyle wf$解釋:
:::success
$\mathcal{B}$和$\mathcal{C}$是$\displaystyle wfs$。$\displaystyle A_{i}^{n}$是n元謂詞符號。變數的取值為${\{a_i\}}_{i\in\mathbb{N}}$之下,項$\displaystyle t_1, t_2, ....,t_n$的取值分別為$\displaystyle {(t_1)}_M, {(t_2)}_M, ...., {(t_n)}_M$,則
(1)${\{a_i\}}_{i\in\mathbb{N}}$滿足$\displaystyle A_{i}^{n}(\displaystyle t_1, t_2, ....,t_n)$當且僅僅當$\displaystyle ({(t_1)}_M, {(t_2)}_M, ...., {(t_n)}_M)\in {(A_{i}^{n})}_M$ (項對應值組成的有序對,在謂詞符號所對應的關係裡)
(2)${\{a_i\}}_{i\in\mathbb{N}}$滿足$\neg\mathcal{B}$當且僅僅當${\{a_i\}}_{i\in\mathbb{N}}$不滿足$\mathcal{B}$ (否定的直觀定義)
(3)${\{a_i\}}_{i\in\mathbb{N}}$滿足$\mathcal{B}\Rightarrow\mathcal{C}$當且僅僅當${\{a_i\}}_{i\in\mathbb{N}}$不滿足$\mathcal{B}$或是${\{a_i\}}_{i\in\mathbb{N}}$滿足$\mathcal{C}$ (去除滿足$\mathcal{B}$卻不滿足$\mathcal{C}$的狀況)
(4)${\{a_i\}}_{i\in\mathbb{N}}$滿足$(\forall x_j)\mathcal{B}$當且僅當所有$i\neq j$則$\displaystyle c_i=b_i$的變數取值${\{c_i\}}_{i\in\mathbb{N}}$滿足$\mathcal{B}$ (第$\displaystyle j$個變數在$\displaystyle D$任意取值要為真)
:::
### 真假值與邏輯
由邏輯符號的語意,我們可以理解合式公式在解釋$\displaystyle M$下的"真假":
:::success
(1)合式公式$\mathcal{B}$在$\displaystyle M$為真當且僅僅當每組變數取值都滿足$\mathcal{B}$,以符號${\models}_{M}\mathcal{B}$表示。
(2)合式公式$\mathcal{B}$在$\displaystyle M$為假當且僅僅當每組變數取值都不滿足$\mathcal{B}$。
(3)$\displaystyle\Gamma$是一組一階邏輯的$\displaystyle wfs$,如果所有$\displaystyle\Gamma$的$\displaystyle wf$在解釋$\displaystyle M$下都是真的,稱$\displaystyle M$是$\displaystyle\Gamma$的**模型**(model)
:::
甚至一些合式公式是不隨解釋的選取而總是為真,也就是說,他在"邏輯上"就是正確的
:::success
如果對於任何解釋$\displaystyle M$,${\models}_{M}\mathcal{B}$,稱$\mathcal{B}$為**邏輯上有效的**(logically valid)。反之對於任何解釋都為假的$\mathcal{B}$稱為**邏輯上無效的**(logically invalid)或是直稱**矛盾**。
:::
一階邏輯形式理論裡的邏輯定理,依照我的們的期望理當是邏輯上有效的$\displaystyle wf$。其實一階邏輯的邏輯上有效,就是仿造命題邏輯的恆等式定義的。
類似的,我們也可以定義**邏輯上等價**和**邏輯上推出**:
:::success
對於合式公式$\mathcal{B}$和$\mathcal{C}$
(1)**$\mathcal{B}$在邏輯上推出$\mathcal{C}$**當且僅僅當對於任何解釋,滿足$\mathcal{B}$的變數取值也會滿足$\mathcal{C}$
: (也就是當且僅僅當$\mathcal{B}\Rightarrow\mathcal{C}$是邏輯上有效的)
(2)$\mathcal{B}$是一套$\displaystyle wfs$(也就是$\displaystyle\Gamma$)的**邏輯結論**(logical consequence),當且僅僅當對於任何解釋,滿足所有$\displaystyle\Gamma$的$\displaystyle wf$的變數取值,也會滿足$\mathcal{B}$。
(3)**$\mathcal{B}$在邏輯上等價於$\mathcal{C}$**當且僅僅當對於他們邏輯上可以推出彼此
: (也就是當且僅僅當$\mathcal{B}\Leftrightarrow\mathcal{C}$是邏輯上有效的)
:::
### 重要的邏輯有效式
## 型式理論
(I)符號:
:::success
(1)量詞:$\forall$
(2)命題連接詞(propositional connectives):$\neg,\Rightarrow$
(3)標點符號:逗號跟左右括弧。(但為了更方便閱讀命題連接詞施用的順序,我們會額外採用中括弧跟大括弧)
(4)一定要有,但最多跟跟自然數一樣多的變數符號。特定變數用有下標的$x$代表,如$x_1,\,x_2,\,....$;其他小寫的任何西方語言字母,就算有上下標或是prime,若沒有特別申明,僅僅代表任意的變數,如$a,\,\beta',\gamma_3,\,\delta^4,\,\aleph^5_5$
(5)可能有函數符號,可能有常數。**但一定會有謂詞符號**。這些符號都最多可以跟自然數一樣多。
:::
: 另外,我們用大寫西方字母代表**項**,如$T,\,\Gamma$。
: 有時候謂詞符號和函數符號裡有大量的變數,為求簡便起見,我們以${\big{<}a_k\big{>}}^{n}_{k=1}$ 代表 $a_1,....,\,a_n$;而項亦採用這個方法,將$T_1,....,\,T_n$簡記為${\big{<}T_k\big{>}}^{n}_{k=1}$。
(II)合式公式($\displaystyle wf$):
:::success
(1)所有原子公式是$\displaystyle wf$。
(2)如果$\mathcal{B},\mathcal{C}$是$\displaystyle wf$,$\displaystyle y$是一個變數,則$(\neg\mathcal{B}),(\mathcal{B}\Rightarrow\mathcal{C}),((\forall y)\mathcal{B})$都是$\displaystyle wf$。最外層的括弧,和包住$\forall y$的括弧,如果命題連接詞施用的順序很明顯可以不用寫。
(3)$\displaystyle wf$只能從上面兩點建構出來。
:::
: 沒有特別聲明的話,我們習慣用草寫的大寫字母代表$\displaystyle wf$;另外為了辨別方便,我們會對$\displaystyle wf$加上數字上下標或是prime,如${\mathcal{B}}_1$、$\mathcal{B}'$。
(III)公理:
: $\displaystyle (a)$邏輯公理:如果$\mathcal{B},\mathcal{C},\mathcal{D}$是$\displaystyle wf$
:::success
(A1)$\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{B})$
(A2)$[\mathcal{B}\Rightarrow(\mathcal{C}\Rightarrow\mathcal{D})]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{D})]$
(A3)$[(\neg\mathcal{B})\Rightarrow(\neg\mathcal{C})]\Rightarrow[(\neg\mathcal{B}\Rightarrow\mathcal{C})\Rightarrow\mathcal{B}]$
(A4)$\displaystyle T$是一個項(裡面出現的變數記為$\displaystyle t_j$);$\displaystyle x$是一個變數。如果在$\mathcal{B}$裡面,所有$\displaystyle t_j$的量詞的範圍裡都沒有自由的$\displaystyle x$(這個情況稱在$\mathcal{B}$項$\displaystyle T$對$\displaystyle x$是自由的),則
: $[(\forall x)\mathcal{B}(x)]\Rightarrow[\mathcal{B}(T)]$
$\mathcal{B}(T)$代表把$\mathcal{B}$裡自由的$\displaystyle x$都取代為$\displaystyle T$
(A5)如果在$\mathcal{B}$裡面,都沒有自由的$\displaystyle x$則
: $[(\forall x)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[\mathcal{B}\Rightarrow(\forall x)(\mathcal{C})]$
(A6)若$\mathcal{B}$是公理,則
: $(\forall a_1)(\forall a_2)....(\forall a_n)\mathcal{B}$
也是公理。
(A7)$[(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{B}\Rightarrow\mathcal{C})]\Rightarrow[(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{B})\Rightarrow(\forall x_1)(\forall x_2)....(\forall x_n)(\mathcal{C})]$
:::
: 關於取代,我們根據(A4)做出以下的符號規定;合式公式表示成$\mathcal{B}(a_1,\,....,\,a_n)$不代表$\mathcal{B}$只有$a_1,\,....,\,a_n$是自由的;這僅僅是因為$\mathcal{B}(T_1,\,....,\,T_n)$代表每個出現自由$a_k$的位置,分別被項$T_k$所取代。
: ex.若以$\mathcal{B}(x,\,y)$代表$(\forall x)[A^{3}_1(x,\,y,\,z)]\Rightarrow(\forall y)[A^{3}_2(x,\,y,\,z)]$,那$\mathcal{B}(T,\,S)$的意思是
: $(\forall x)[A^{3}_1(x,\,T,\,z)]\Rightarrow(\forall y)[A^{3}_2(S,\,y,\,z)]$
: $\displaystyle (b)$真公理(proper axioms):根據不同理論的需求而訂製。
(IV)推理規則:如果$\mathcal{B},\mathcal{C}$是$\displaystyle wf$,$\displaystyle x$是一個變數
:::success
MP律:$(\mathcal{B}\Rightarrow\mathcal{C})$跟$\mathcal{B}$可以推出$\mathcal{C}$。
:::
其他的邏輯符號如下定義:
:::success
$\mathcal{A}\wedge\mathcal{B}: =\neg[\mathcal{A}\Rightarrow\neg(\mathcal{B})]$
$\mathcal{A}\vee\mathcal{B}: =(\neg \mathcal{A})\Rightarrow \mathcal{B}$
$(\exists x)(\mathcal{A}): =\neg[(\forall x)(\neg \mathcal{A})]$
:::
而簡寫的規則,我們僅需將**括弧規則**第二項的施用順序改成
:::success
$\neg,\,\wedge,\,\vee,\,\forall,\,\Rightarrow,\,\Leftrightarrow$
:::
注意到一階邏輯$wf$的遞迴定義雖然和命題邏輯的不同,但這種差異不影響推論元定理依據(A1)、(A2)和(A3)的形式做出的證明,故推論元定理可以在一階邏輯沿用。
(A4)是一切取代的最終極基礎。所以為了方便起見,套用(T)和(DN)以後,我們可以得到(A4)的"$\exists$"形式:
:::success
(A4e)
若於$\mathcal{B}(x)$,$T$對$x$是自由的,則
$\vdash\mathcal{B}(T)\Rightarrow(\exists x)\mathcal{B}(x)$
:::
## 變數變換
像"所有在美國領土出身且非外敵侵略者的後代的人,都是美國公民",採用哪一個變數在直觀上是沒有差別的。這乃因"人"這個變數在這段敘述裡是自由的。更一般的來說,我們有已下定理
:::success
**定理**:($ChV$, change of variable)
$\mathcal{B}(y)$是以$y$取代$\mathcal{B}(x)$內自由的$x$而成,若:
>(1)在$\mathcal{B}(x)$項$x$對$y$是自由的(i.e. $\mathcal{B}(x)$內$y$的量詞範圍內沒有自由的$x$)
>(2)$\mathcal{B}(x)$理沒有自由的$y$
(此種狀況稱為$\mathcal{B}(x)$**相似於**(similar to)$\mathcal{B}(y)$)
則
>$(I)$ $\mathcal{B}(y)$也相似於$\mathcal{B}(x)$
>$(II)$ $\vdash(\forall x)\mathcal{B}(x)\Leftrightarrow(\forall y)\mathcal{B}(y)$
>$(III)$ $\vdash(\exists x)\mathcal{B}(x)\Leftrightarrow(\exists y)\mathcal{B}(y)$
**證明**:
<details>
$(I)$
>首先$\mathcal{B}(y)$自由的$x$都被取代光了,而取代後,自由的$y$是來自於自由的$x$,所以它們更不可能出現在$x$的量詞範圍內。由此可以確定$\mathcal{B}(y)$也相似於$\mathcal{B}(x)$。
$(II)$
>(1) $(\forall x)\mathcal{B}(x)\Rightarrow\mathcal{B}(y)$ (A4)
>(2) $(\forall x)\mathcal{B}(x)\Rightarrow(\forall y)\mathcal{B}(y)$ (MP with 1, A5)
>因為$\mathcal{B}(y)$也相似於$\mathcal{B}(x)$。我們可以同法得到
>$\vdash(\forall y)\mathcal{B}(y)\Rightarrow(\forall x)\mathcal{B}(x)$
$(III)$
>$取\mathcal{C}(x)\asymp\neg\mathcal{B}(x)$套入$(II)$有
>$(\forall x)[\neg\mathcal{B}(x)]\Rightarrow(\forall y)[\neg\mathcal{B}(y)]$
>再套用(T)就有
>$(\exists x)\mathcal{B}(x)\Rightarrow(\exists y)\mathcal{B}(y)$
>反向同理。$\Box$
</details>
:::
## 推廣律
公理(A7)可以稍加延伸,跟我們的直觀連繫在一起
:::success
**元定理**(定理的推廣律):
$\ulcorner\vdash\mathcal{B}\urcorner\to\ulcorner\vdash(\forall x)\mathcal{B}\urcorner$
**證明**
<details>
假設$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$就是$\mathcal{B}$的證明,那$\mathcal{C}_1$一定是公理,根據(A6)可以得到$\vdash(\forall x)\mathcal{C}_1$
若對$\displaystyle i<k$都有$\vdash(\forall x)\mathcal{C}_i$,如果$\mathcal{C}_k$是公理的話顯然$\vdash(\forall x)\mathcal{C}_k$;所以我們考慮有$\displaystyle l,m<k$使得
$\mathcal{C}_m: \mathcal{C}_l\Rightarrow\mathcal{C}_k$。
則根據歸納法的假設跟(A7)
$\vdash(\forall x)\mathcal{C}_l\Rightarrow(\forall x)\mathcal{C}_k$
配上$\vdash(\forall x)\mathcal{C}_l$就可以得到$\vdash(\forall x)\mathcal{C}_k$,以此歸納到$\mathcal{C}_n$也就是$\mathcal{B}$,故本元定理得證$\Box$。
</details>
:::
以下就是最一般情況的**推廣律**。
:::success
**元定理**($\displaystyle GEN$, Rule of Generalization):
$\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n$裡都沒有自由的$\displaystyle x$,則
$\ulcorner\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash\mathcal{B}\urcorner\to\ulcorner\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_n\vdash(\forall x)\mathcal{B}\urcorner$
**證明**
<details>
我們對前提條件的數量$\displaystyle n$做歸納。
若$\displaystyle n = 1$,前提條件就是$\mathcal{A}_1\vdash\mathcal{B}$,則根據推論元定理跟定理的推廣律,會得到$\vdash(\forall x)(\mathcal{A}_1\Rightarrow\mathcal{B})$,再根據(A6)和MP律,就可以得到$\vdash\mathcal{A}_1\Rightarrow(\forall x)\mathcal{B}$,也就是本元定理要求的結果。
現在假設$\displaystyle n < k$的情況下元定理會成立,若$\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_{k-1}\vdash\mathcal{A}_k\Rightarrow\mathcal{B}$,根據歸納法的假設
$\mathcal{A}_1,\mathcal{A}_2,....,\mathcal{A}_{k-1}\vdash(\forall x)(\mathcal{A}_k\Rightarrow\mathcal{B})$
配上(A5),本元定理在$\displaystyle n = k$的情況就可以得到證明,故本元定理得證$\Box$。
</details>
:::
(GEN)可以稍加修飾,以適合證明"$\exists$"形式的定理(以後簡稱GENe)
:::success
**元定理**:
若$\displaystyle x$在$\displaystyle \Gamma$裡的$\displaystyle wfs$裡面都不自由,且$\mathcal{C}$裡也沒有自由的$\displaystyle x$
(1) $\ulcorner\Gamma\vdash\mathcal{A}\Rightarrow\mathcal{B}\urcorner\to\ulcorner\Gamma\vdash(\exists x)\mathcal{A}\Rightarrow(\exists x)\mathcal{B}\urcorner$
(2) $\ulcorner\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\urcorner\to\ulcorner\Gamma\vdash(\exists x)\mathcal{B}\Rightarrow\mathcal{C}\urcorner$
**證明提示**:使用(T)和(A5)
:::
由推廣律,很容易證明以下關於"交換性"的定理
:::success
(1) $(\forall x)(\forall y)\mathcal{A}\vdash(\forall y)(\forall x)\mathcal{A}$
(2) $(\exists x)(\exists y)\mathcal{A}\vdash(\exists y)(\exists x)\mathcal{A}$
(3) $(\exists x)(\forall y)\mathcal{A}\vdash(\forall y)(\exists x)\mathcal{A}$
:::
注意最後一個定理是一般來說是不能反向的,只要想到"對每個a,都有一個數(也就是$\displaystyle -a$),使$\displaystyle a+(-a)=0$",但是任取一個$\displaystyle a$的數$\displaystyle (-a)$和任意的數$\displaystyle b$,$\displaystyle b+(-a)$並不一定會為零。
## 量詞表示的簡化
為了讓我們的敘述更好閱讀,對於變數$\displaystyle x_1,x_2,....,x_n$和任意變數$\displaystyle x,y$、合式公式$\mathcal{B}$、和可被簡記為$x\star y$的$\displaystyle A_{i}^{2}(x,y)$,我們定義:
:::success
$(\forall x\star y)(\mathcal{B}): =(\forall x)[(x\star y)\Rightarrow\mathcal{B}]$
$(\exists x\star y)(\mathcal{B}): =(\exists x)[(x\star y)\wedge\mathcal{B}]$
$(x_1,x_2,....,x_n\star y): =(x_1\star y)\wedge(x_2\star y)\wedge\,....\,\wedge(x_n\star y)$
:::
也就是我們平常的"屬於"、"等於"都可以用這個方式簡寫
直觀上我們比較常說"對所有a屬於A且滿足....的話....則...."會不會不會跟上面的話簡化符號有所牴觸呢?為了回答這個問題,首先有以下定理:
:::success
(abb)$\vdash[\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})]\Leftrightarrow[(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}]$
**證明**
<details>
($\Rightarrow$) $\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})\vdash(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}$
注意到
$\mathcal{A}\wedge\mathcal{B}\vdash\mathcal{A}$
$\mathcal{A}\wedge\mathcal{B}\vdash\mathcal{B}$
所以
$\mathcal{A}\wedge\mathcal{B},\,\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})\vdash\mathcal{C}$
再由推論元定理就可以得證。$\Box$
($\Leftarrow$) $(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}\vdash\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$
注意到
$\mathcal{A},\,\mathcal{B}\vdash\mathcal{A}\wedge\mathcal{B}$
所以
$(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C},\,\mathcal{A},\,\mathcal{B}\vdash\mathcal{C}$
再由推論元定理就可以得證。$\Box$
</details>
:::
由此就可以證明以下定理($x\star y$代表$\displaystyle A_{i}^{2}(x,y)$;$x\ast y$代表$\displaystyle A_{j}^{2}(x,y)$)
:::success
$\vdash(\forall x\star T)(\forall y\ast S)\mathcal{B}\Leftrightarrow\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$
其中$\displaystyle S$是項;$\displaystyle y$不出現在項$\displaystyle T$中
**證明**
<details>
($\Rightarrow$) $(\forall x\star T)(\forall y\ast S)\mathcal{B}\vdash\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$
(1)$\forall x\{(x\star T)\Rightarrow\forall y[(y\ast S)\Rightarrow\mathcal{B}]\}$ (Hyp)
(2)$(x\star T)\Rightarrow\forall y[(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 1, A4)
(3)$(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]$ (D1 with 2, A4)
(4)$[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}$ (MP with 3, abb)
(5)$\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}$ (GEN with 4 twice)
($\Leftarrow$) $\forall x\forall y\{[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}\}\vdash(\forall x\star T)(\forall y\ast S)\mathcal{B}$
(1)$\forall x\forall y\{[(x\star T)\wedge(y\ast S)\Rightarrow\mathcal{B}]$ (Hyp)
(2)$[(x\star T)\wedge(y\ast S)]\Rightarrow\mathcal{B}$ (MP with 2, A4 twice)
(3)$(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 2, abb)
(4)$\forall y\{(x\star T)\Rightarrow [(y\ast S)\Rightarrow\mathcal{B}]\}$ (GEN with 3)
(5)$(x\star T)\Rightarrow \forall y[(y\ast S)\Rightarrow\mathcal{B}]$ (MP with 4, A5)
(6)$\forall x\{(x\star T)\Rightarrow \forall y[(y\ast S)\Rightarrow\mathcal{B}]\}$ (GEN with 5)
</details>
:::
由以上的定理,可以歸納出更多變數狀況的簡化式,且簡化式前面的括弧可以"交換"的條件,是括弧中的項不能出現別的括弧裡的變數。
更一般來說,仿照上面的證明,定理可以延伸為
:::success
$\vdash(\forall x)[\mathcal{A}\Rightarrow(\forall y)(\mathcal{B}\Rightarrow\mathcal{C})]\Leftrightarrow(\forall x)(\forall y)[(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}]$
其中$\displaystyle y$在$\mathcal{A}$裡不是自由的。
:::
這個一般化定理之後將大大減化**集合]]論的定理的推導和表示。
我們可以對"$\exists$"得出類似的定理
:::success
$(\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})]$
:::
但反過來是不對的,因為$\mathcal{A}\wedge(\exists y)\mathcal{D}$不總是能推出$\mathcal{A}\wedge\mathcal{D}$。
## 等號
若一階邏輯的型式理論,配有一謂詞符號$A^{2}_{i}(x,y)$(簡記為$\displaystyle x = y$),使下列$\displaystyle wfs$為此形式理論的**定理**:
:::success
(E1) $\displaystyle x=x$ (等號的自反性)
(E2) $(x=y)\Rightarrow[\mathcal{B}(x,x)\Rightarrow\mathcal{B}(x,y)]$ (等號的可代換性)
其中在$\mathcal{B}(x,x)$中$\displaystyle y$對$\displaystyle x$是自由的;而$\mathcal{B}(x,y)$是由$\mathcal{B}(x,x)$裡**一些**自由的$\displaystyle x$被取代成$\displaystyle y$而成的
:::
則稱這個型式理論是**帶等號**的一階邏輯(with equality)。把(E1)和(A4)組合起來,很自然的確保"有人一定會跟指定數相等":
:::success
$\vdash(\forall x)(\exists y)(x=y)$
:::
### 等號的性質
以下定理是帶等號的一階邏輯的基本性質($\displaystyle T$, $\displaystyle S$, $\displaystyle R$都是**項**)
:::success
**(I)** $\vdash T=T$
**證明提示**:取一個$\displaystyle T$中沒出現的變數,以對(E1)應用GEN後應用(A4)。
:::
:::success
**(II)** $\vdash (T=S)\Rightarrow(S=T)$
**證明**
<details>
(1)$(x=y)\Rightarrow[(x=x)\Rightarrow(y=x)]$ (E2)
(2)$(x=y)\Rightarrow(y=x)$ (D2 with E1, 1)
(3)$\forall x\forall y[(x=y)\Rightarrow(y=x)]$ (GEN)
現在取$\displaystyle x$為不在$\displaystyle T$中的變數;$\displaystyle y$取為不在$\displaystyle S$中的變數。套用兩次(A4),定理就可以得證。$\Box$
</details>
:::
:::success
**(III)** $\vdash (T=S)\Rightarrow[(S=R)\Rightarrow(T=R)]$
**證明**
<details>
(1)$(y=x)\Rightarrow[(y=z)\Rightarrow(x=z)]$ (E2)
(2)$(x=y)\Rightarrow[(y=z)\Rightarrow(x=z)]$ (D1 with II, 1)
(3)$\forall x\forall y\forall z\{(x=y)\Rightarrow[(y=z)\Rightarrow(x=z)]\}$ (GEN)
現在取$\displaystyle x$為不在$\displaystyle T$中的變數;$\displaystyle y$取為不在$\displaystyle S$中的變數;$\displaystyle z$取為不在$\displaystyle R$中的變數。套用三次(A4),定理就可以得證。$\Box$
</details>
:::
**Kronecker符號**被定義為相等的時候為1,不相等的時候則為零,以下的元定理,將奠定這種直觀定義的基礎。
:::success
(DC, Definition under certain condition)
若$x$於$\mathcal{A}$不自由,$c$是常數則
$\ulcorner\,\mathcal{A}\vdash(\exists x)\mathcal{B}\,\urcorner\to\ulcorner\,\vdash(\exists x)\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}\,\urcorner$
**證明**:
<details>
(1) $\mathcal{A}\Rightarrow(\exists x)\mathcal{B}$ (Hyp)
(2) $(\forall x)\{\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}\}$ (Hyp)
(3) $\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}$ (MP with A4, 2)
(4) $\neg[\neg\mathcal{A}\wedge(x=c)]\wedge\neg(\mathcal{A}\wedge\mathcal{B})$ (MP with 3, DIS)
(5) $\neg[\neg\mathcal{A}\wedge(x=c)]$ (MP with AND,4)
(6) $\neg(\mathcal{A}\wedge\mathcal{B})$ (MP with AND, 4)
(7) $\neg\mathcal{A}\Rightarrow\neg(x=c)$ (MP with DIS, DN 5)
(8) $\mathcal{A}\Rightarrow\neg\mathcal{B}$ (MP with DIS, DN, 5)
(9) $\mathcal{B}\Rightarrow\neg\mathcal{A}$ (MP with T, 8)
(10) $(\exists x)\mathcal{B}\Rightarrow\neg\mathcal{A}$ (GENe with 9)
(11) $\mathcal{A}\Rightarrow\neg(\exists x)\mathcal{B}$ (MP with T, 11)
(12) $\neg\mathcal{A}$ (A3' with 1, 11)
(13) $\neg(x=c)$ (MP with 7, 12)
(14) $(\forall x)[\neg(x=c)]$ (GEN with 13)
再套用一次DN也就是
$\mathcal{A}\Rightarrow(\exists x)\mathcal{B}\,\vdash(\forall x)\{\neg\{[\neg\mathcal{A}\wedge(x=c)]\vee(\mathcal{A}\wedge\mathcal{B})\}\}\Rightarrow\neg(\exists x)(x=c)$
但由上面的性質I有
$\vdash c=c$
再對$x$套用一次(A4e)有
$\vdash(\exists x)(x=c)$
所以由(C2)就會得到我們想證明的結果。$\Box$
</details>
:::
### (E2)的等價條件
:::success
**元定理**:
(E2)等價於要求以下兩點
(1)對於**不含函數符號、常數**的原子公式$\mathcal{B}(x,x)$有
: $x=y\vdash \mathcal{B}(x,x)\Rightarrow \mathcal{B}(x,y)$
: 其中$\mathcal{B}(x,y)$來自於$\mathcal{B}(x,x)$中一個$\displaystyle x$被取代為$\displaystyle y$
(2)對於任意函數符號$\displaystyle f_i^n(x_1,....,x_j,....,x_n)$有
: $a_k=x\vdash f_i^n(a_1,....,\,a_k,....,\,a_n) = f_i^n(a_1,....,\,x,....,\,a_n)$($\displaystyle a_k$被$\displaystyle x$取代)
**證明**
<details>
從(E2)推理出兩點是很顯然的,因為(1)是(E2)的特殊情況;而(2)只不過是(E2)的特殊狀況套用(D2)而已。
現在我們從這兩點推出一般狀況的(E2)。
**(I)擴張到有含常數的原子公式**
: 如果對含常數$\displaystyle c$(但不含函數符號!)的原子公式$\mathcal{B}(x,x,c)$,目標是證明$x=y\vdash \mathcal{B}(x,x,c)\Rightarrow \mathcal{B}(x,y,c)$,那從(1),如果取一個和$\displaystyle x$和$\displaystyle y$都不同的變數$\displaystyle z$,則
: $\vdash (x=y)\Rightarrow[\mathcal{B}(x,x,z)\Rightarrow \mathcal{B}(x,y,z)]$
: 也就是把目標$\displaystyle wf$有常數的地方都換成變數$\displaystyle z$。這樣,對上面的定理以$\displaystyle z$使用(GEN),然後用(A4)把$\displaystyle z$都換為$\displaystyle c$,就會推出我們的目標。
: 如果原子公式含有多個(以符號的基礎上辨別為)相異的常數,那連續以上面的方法,將相異常數替換為相異變數,一樣可以在有限步驟內推出我們的目標
**(II)擴張到含函數符號的原子公式**
: 原子公式的形式如$\displaystyle A^m_j(T_1,....,T_k,....,T_m)$,而項$\displaystyle T_k$裡中的一個$\displaystyle x$被取代成$\displaystyle y$以後,變成$\displaystyle S$,我們的目標就是證明
: (注意到函數符號沒有被取代的狀況,取沒有出現的變數套用A4即可)
: $\vdash (x=y)\Rightarrow[A^m_j(T_1,....,T_k,....,T_m)\Rightarrow A^m_j(T_1,....,S,....,T_m)]$
: 顯然我們只需要證明
: $\vdash (x=y)\Rightarrow[A^m_j(x,....,T_k,....,z)\Rightarrow A^m_j(x,....,S,....,z)]$(*)
: 其中這些新加入的變數都沒有出現在原來的項中,那連續對上式套用(GEN)和(A4),就可以得到我們的目標結果。但進一步的
: (A)$\vdash (a=b)\Rightarrow[A^m_j(x,....,a,....,z)\Rightarrow A^m_j(x,....,b,....,z)]$($\displaystyle a$不出現在項$\displaystyle T_k$裡;$\displaystyle b$不出現在項$\displaystyle S$裡)
: (B)$\vdash (x=y) \Rightarrow(T_k=S)$
: (A)式先連續對$\displaystyle a$和$\displaystyle b$使用(GEN)後,再連續兩次使用(A4),然後和(B)以(D1)結合,就可以得到(*)。但(A)其實就是(I)已經證明的前提,實際上只有(B)需要證明。
: 為了證明(B),我們要針對項$\displaystyle T_k$裡出現的函數符號數量進行歸納:(因為項是"遞迴"定義)
: 在函數符號的數量為 0 的狀況僅僅是$\vdash (x=y)\Rightarrow(x=y)$,顯然為真。
: 函數符號的數量為 1 的狀況,如果不含常數就是本元定理的條件(2);若含常數的話仿造(I)的方法,取一些不曾出現的變數替換常數後套用(A4),就可以從條件(2)推出。故數量為1的情況(B)都正確。
: 現在假設函數符號的數量小於$\displaystyle n$的時候(B)都正確,那根據項的定義,函數符號的數量為$\displaystyle n$的項可以寫成
: $\displaystyle f^l_k(S_1,....,S_k,....,S_l)$
: 其中項$\displaystyle S_1$到$\displaystyle S_l$內含數量小於$\displaystyle n$的函數符號,**但這些內含的函數符號數量總和會是$\displaystyle n-1$**。那事實上我們要證明
: $\vdash(x=y)\Rightarrow[f^l_k(S_1,....,S_k,....,S_l)=f^l_k(S_1,....,R,....,S_l)]$(項$\displaystyle R$是項$\displaystyle S_k$中的一個$\displaystyle x$被取代為$\displaystyle y$而成)
: 但只要把沒被$\displaystyle y$取代的項換成不曾出現的變數,套用(A4)加上歸納前提,上式就可以得到證明,故(B)在所有情況都是正確的。所以我們已經證明了(II)的目標。
**(III)一般$\displaystyle wf$的情況**
: 因為原子公式也是$\displaystyle wf$,所以證明一般$\displaystyle wf$添加量詞和命題連接詞後的新$\displaystyle wf$也符合(E2)取代一次的情況,就等同於對一般$\displaystyle wf$內的量詞和命題連接詞數量做歸納。
: 首先考慮添加量詞的情況;如果前提是
: $\vdash (x=y)\Rightarrow[\mathcal{B}(x,x)\Rightarrow \mathcal{B}(x,y)]$ (**)
: 那我們的目標是
: $\vdash (x=y)\Rightarrow[(\forall z)\mathcal{B}(x,x)\Rightarrow (\forall z)\mathcal{B}(x,y)]$ ($\displaystyle z$異於$\displaystyle x$和$\displaystyle y$)
: 新添加的量詞變數不能是$\displaystyle x$或是$\displaystyle y$,否則自由的$\displaystyle x$或是$\displaystyle y$會變成通通不自由,就沒有取代的意義。
: 對(**)以變數$\displaystyle z$使用(GEN)以後,套用(A4)然後(A7)就會達到我們的目標
: 再來是添加命題連接詞的部分;為了考慮添加"$\Rightarrow$"的部分,我們額外加上下列(歸納)前提
: $\vdash (x=y)\Rightarrow[\mathcal{C}(x,x)\Rightarrow \mathcal{C}(x,y)]$
: $\vdash (y=x)\Rightarrow[\mathcal{B}(x,y)\Rightarrow \mathcal{B}(x,x)]$(***)
: 那我們的目標就是
: $\vdash (x=y)\Rightarrow\{[\mathcal{B}(x,x)\Rightarrow\mathcal{C}(x,x)]\Rightarrow[\mathcal{B}(x,y)\Rightarrow\mathcal{C}(x,x)]\}$
: $\vdash (x=y)\Rightarrow\{[\mathcal{B}(x,x)\Rightarrow\mathcal{C}(x,x)]\Rightarrow[\mathcal{B}(x,x)\Rightarrow\mathcal{C}(x,y)]\}$
: 考慮到(D1)
: $\mathcal{D}\Rightarrow\mathcal{E},\,\mathcal{E}\Rightarrow\mathcal{E}'\vdash\mathcal{D}\Rightarrow\mathcal{E}'$
: $\mathcal{D}'\Rightarrow\mathcal{D},\,\mathcal{D}\Rightarrow\mathcal{E}\vdash\mathcal{D}'\Rightarrow\mathcal{E}$
: 套用上推論元定理,就可以證明我們的目標。
: 最後對"$\neg$",我們的目標是
: $\vdash (x=y)\Rightarrow\{[\neg\mathcal{B}(x,x)]\Rightarrow [\neg\mathcal{B}(x,y)]\}$
: 但考慮到(***),然後套用(T)的話,目標就可以得到證明。
最後,雖然我們以上證明的都是取代一次的狀況,但是取代$\displaystyle n$次的情況,可以視為被取代$\displaystyle n-1$次的情況再取代一次;所以我們可以用取代一次的情況歸納到任意數量的取代,故(1)、(2)的要求和(E2)是等價的$\Box$
</details>
:::
### 唯一性
:::success
$(\exists! x)\mathcal{B}(x): =(\exists x)\mathcal{B}(x)\wedge(\forall x)(\forall \xi)\{[\mathcal{B}(x)\wedge\mathcal{B}(\xi)]\Rightarrow (x=\xi)\}$
其中 $\xi$ 是任何不出現在$\mathcal{B}(x)$的變數。
:::
## 函數符號與唯一性
數學理論常常隨著內容的推進,而需要符號上的簡化;也就是一套型式理論增加新的符號(函數符號、常數符號)以後,我們仍然希望這個"新"型式理論和原來的型式理論,有同等的效力。具體來說,對每個新系統裡的合式公式$\displaystyle\mathcal{B}$,有一個符號上的變換,將$\displaystyle\mathcal{B}$轉變為原來理論中的合式公式$\displaystyle\mathcal{B}'$,並滿足
:::success
(1)若 $\mathcal{B}$ 只包含舊理論的符號,則 $\mathcal{B}^{\prime} \asymp \mathcal{B}$
(2)$\vdash_n\mathcal{B}\Leftrightarrow\mathcal{B}'$
(3)$\ulcorner\,\vdash_n\mathcal{B}\,\urcorner\to\ulcorner\,\vdash_o\mathcal{B}'\,\urcorner$
:::
其中,$\vdash_o$代表可於舊理論內推出;$\vdash_n$代表可於新理論內推出。
由(2)可以推出$\ulcorner\,\vdash_o\mathcal{B}'\,\urcorner\to\ulcorner\,\vdash_n\mathcal{B}\,\urcorner$,因為舊理論擁有的符號比較少,所以 $\mathcal{B}^{\prime}$ 本來就處在新理論的表述範圍內,所以$\ulcorner\,\vdash_o\mathcal{B}^{\prime}\,\urcorner\to\ulcorner\,\vdash_n\mathcal{B}^{\prime}\,\urcorner$,這樣配上定義(2)的確可以在新理論內推出 $\mathcal{B}$。
綜上所述,以上的定義的確達到了「新舊理論效力等同」的要求!
### 直觀的動機
直觀上「任何數都有相反數」──也就是說
:::success
對每個$x$存在唯一的$y$使得$x+y=0$
:::
習慣上會以符號「$-x$」來代表相反數,換句話說
:::success
$x+(-x)=0$
:::
那一般來說,若變數$a_1,\,\ldots,a_n,\,x$在$\mathcal{B}$裡自由且
:::success
$\vdash_o(\exists!x)\mathcal{B}(a_1,\,\ldots,a_n,\,x)$
:::
那應該可以添加一個新的$n$元函數符號$f^{n}_i$,和作為它的「定義」的新公理
:::success
$\mathcal{B}[a_1,\,\ldots,\,a_n,\,f^{n}_i(a_1,\,\ldots,\,a_n)]$
:::
那新舊理論的$wfs$要如何做符號轉換呢?比如說,「相反數大於零」這個敘述明顯是**新理論**裡的敘述;那在**舊理論**,應該敘述成「對每個 $x$ ,存在$y$不但$x+y=0$且$y>0$」
所以一般來說若
:::success
$\mathcal{C}[\ldots,\,f(T_1,\,\ldots,\,T_n),\ldots]$
:::
是新理論裡的$wf$,那它應該對應到舊理論裡的
:::success
$(\exists x)[\mathcal{C}(\cdots,\,x,\,\ldots)\wedge\mathcal{B}]$
:::
注意到不管是新舊理論,相反數的唯一性存在性都是個定理。
### 一個唯一性的定理
在以嚴謹的方式實踐以上的直觀的動機前,需要一個輔助定理
:::success
$(\exists! x)\mathcal{B}(x)\vdash(\exists x)[\mathcal{B}(x)\wedge\mathcal{C}(x)]\Leftrightarrow(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)]$ (aux)
**證明**
<details>
假設$t$不曾在$\mathcal{B}(x)$和$\mathcal{C}(x)$出現。
($\Rightarrow$)
: (1)$(\forall x)(\forall t)[\mathcal{B}(x)\wedge\mathcal{B}( t)\Rightarrow(x=t)]$ (Hyp)
: (2)$\mathcal{B}(x)\wedge\mathcal{B}(t)\Rightarrow(x=t)$ (MP with A4 twice)
: (3)$\mathcal{B}(t)$ (Hyp)
: (4)$\mathcal{B}(x)\wedge\mathcal{C}(x)$ (Hyp)
: (5)$\mathcal{C}(t)$ (MP with 2, 3, 4)
: 也就是
: $(\exists! x)\mathcal{B}(x),\;\mathcal{B}(x)\wedge\mathcal{C}(x)\vdash\mathcal{B}(t)\Rightarrow\mathcal{C}(t)$
: 再套用(GENe),然後(GEN)可得
: $(\exists! x)\mathcal{B}(x),\;(\exists x)[\mathcal{B}(x)\wedge\mathcal{C}(x)]\vdash(\forall t)[\mathcal{B}(t)\Rightarrow\mathcal{C}(t)]$
: 所以再對$x$套用(A4)和(GEN),就可以得到
: $(\exists! x)\mathcal{B}(x),\;(\exists x)[\mathcal{B}(x)\wedge\mathcal{C}(x)]\vdash(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)]$
($\Leftarrow$)
: (1)$(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)]$ (Hyp)
: (2)$\mathcal{B}(x)$ (Hyp)
: (3)$\mathcal{B}(x)\Rightarrow\mathcal{C}(x)$ (MP with A4, 1)
: (4)$\mathcal{C}(x)$ (MP with 2, 3)
: (5)$\mathcal{B}(x)\wedge\mathcal{C}(x)$($\mathcal{C},\,\mathcal{D}\vdash\mathcal{C}\wedge\mathcal{D}$)
: 也就是
: $(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)],\;\mathcal{B}(x)\vdash\mathcal{B}(x)\wedge\mathcal{C}(x)$
: 套用(GENe),就可以得到
: $(\exists! x)\mathcal{B}(x),\;(\forall x)[\mathcal{B}(x)\Rightarrow\mathcal{C}(x)]\vdash(\exists x)[\mathcal{B}(x)\wedge\mathcal{C}(x)]$ $\Box$
</details>
:::
### 新理論的假設
按照直觀動機一節,需先假設
:::success
$\vdash_o(\exists!x)\mathcal{B}(a_1,\,\ldots,a_n,\,x)$
:::
然後加入新的函數符號$f^{n}_i$和以下的新公理
:::success
$\mathcal{B}[a_1,\,\ldots,a_n,\,f^{n}_i(a_1,\,\ldots,\,a_n)]$ (**U**)
:::
而且還需額外假設,在新理論中,所有的邏輯跟量詞的公理模式都與$f^{n}_i$相容,特別是公理模式(A4),因為它描述**項的代換**。
另外,討論唯一性必須要有等號,所以理當假設新理論是帶等號的形式理論。為了讓等號與新加入的函數符相容,考慮到[(E2)的等價條件](#(E2)的等價條件)必須假設
:::success
$a_k=x\vdash f_i^n(a_1,\ldots,\,a_k,\ldots,\,a_n) = f_i^n(a_1,\ldots,\,x,\ldots,\,a_n)$($\displaystyle a_k$被$\displaystyle x$取代)
:::
由此就可以得到
:::success
$\vdash_n [x=f^{n}_i(a_1,\,\ldots,\,a_n)]\Leftrightarrow\mathcal{B}(a_1,\,\ldots,a_n,\, x)$ (**E**)
**證明**
<details>
($\Rightarrow$)
: 因為有(E2)的存在,配上(A4)我們有
: $[x=f^{n}_i(a_1,\,....,\,a_n)]\Rightarrow\{\mathcal{B}(a_1,\,....,a_n,\, x)\Rightarrow\mathcal{B}[a_1,\,....,a_n,\, f^{n}_i(a_1,\,....,\,a_n)]\}$
: 再配上(D2)和(**U**)就有
: $[x=f^{n}_i(a_1,\,....,\,a_n)]\Rightarrow\mathcal{B}[a_1,\,....,a_n,\, f^{n}_i(a_1,\,....,\,a_n)]$
($\Leftarrow$)
: 對(**U**')套用數次(A4)可得
: $\{\mathcal{B}[a_1,\,....,a_n,\, f^{n}_i(a_1,\,....,\,a_n)]\wedge\mathcal{B}[a_1,\,....,a_n,\,f^{n}_i(a_1,\,....,\,a_n)]\}\Rightarrow[x=f^{n}_i(a_1,\,....,\,a_n)]$
: 再配上(D2)和(**U**)就有
: $\mathcal{B}[a_1,\,....,a_n,\, f^{n}_i(a_1,\,....,\,a_n)]\Rightarrow[x=f^{n}_i(a_1,\,....,\,a_n)]$
</details>
:::
所以(**E**)證實了「跟$f^{n}_i$相等的敘述完全可以用$\mathcal{B}$替代」。
### 符號變換
為了證明新舊理論效力等價的條件(2);先從原子公式開始
:::success
若$x_1,\,\ldots,\,x_n$在舊理論的$\displaystyle\mathcal{A}(x_1,\,\ldots,\,x_n)$裡自由,且$g^{l}_k$是舊理論的函數符號。$T_1,\,\ldots,\,T_n$ 、 $T$ 和 $S_1,\,\ldots,\,S_m$ 是新理論的項,且都不含變數$x$,則
(1)$\displaystyle\vdash_n\mathcal{A}[S_1,\ldots,\,f^{n}_i(T_1,\,\ldots,\,T_m),....,\,S_m]\Leftrightarrow(\exists x)[\mathcal{B}(T_1,\,\ldots,\,T_n,\,x)\wedge \mathcal{A}(S_1,\ldots,\,x,\ldots,\,S_m)]$
(2)
$\displaystyle \mathcal{A}[S_1,\ldots,\,T,\ldots,\,S_m]\Leftrightarrow(\exists x)[\mathcal{B}(T_1,\,\ldots,\,T_m,\,x)\wedge \mathcal{A}(S_1,\ldots,\,x,\ldots,\,S_m)]$
$\vdash_n$
$\mathcal{A}\{S_1,\ldots,\,g^{l}_k[S_1\,\ldots,\,T,\,\ldots,\,S_k],\ldots,\,S_m\}$
$\Leftrightarrow$
$\displaystyle(\exists x)\{\mathcal{B}(T_1,\,\ldots,\,T_n,\,x)\wedge \mathcal{A}(S_1,\ldots,\,g^{l}_k(R_1.\,\ldots,\,x,\,\ldots,\,R_k),\,\ldots,\,S_m)\}$
**證明提示**:
($\Rightarrow$)套用(A4)和(**U**)
($\Leftarrow$)套用上面的(aux),然後用(A4)代換
:::
如此一來,對於原子公式的符號變換就以此遞迴地定義,並以歸納的方式證明條件(2);而一般的$wf$只要對$\neg$和$\Leftrightarrow$的數量做歸納,會得到以下合理的規定
:::success
(1)$(\neg\mathcal{A})'$為$\neg\mathcal{A}'$
(2)$(\mathcal{A}\Rightarrow\mathcal{B})'$為$\mathcal{A}'\Rightarrow\mathcal{B}'$
(3)$(\forall x\mathcal{A})'$為$\forall x\mathcal{A}'$
:::
如此就可以得到一般$wf$下的條件(2)。
### 條件(3)
### 新公理的簡記
如果新的函數符號 $f^n_i$ 是根據(DC)去建立的,也就是說由
:::success
$x$ 於$\mathcal{A}$ 不自由, $a_1,\,\cdots,\,a_n$ 於 $\mathcal{B}$ 完全自由且
$\mathcal{A}\vdash(\exists! x)\mathcal{B}(a_1,\,\cdots,\,a_n,\,x)$
:::
得出新公理 ( $c$ 為一常數符號)
:::success
$\{\neg\mathcal{A}\wedge[\,f^n_i(a_1,\,\cdots,\,a_n)=c]\,\}\vee\{\mathcal{A}\wedge\mathcal{B}[a_1,\,\cdots,\,a_n,\,f^n_i(a_1,\,\cdots,\,a_n)]\}$
:::
那我們會以
:::success
$\begin{cases}
\mathcal{B}[a_1,\,\cdots,\,a_n,\,f^n_i(a_1,\,\cdots,\,a_n)] & \mbox{if }\mathcal{A} \\
f^n_i(a_1,\,\cdots,\,a_n)=c & \mbox{otherwise}
\end{cases}$
:::
簡記這個新公理。由"或"的符號定義和(De Morgan),這個簡記是非常直觀的。