# 一階邏輯

## 簡介
不同於命題邏輯，自一階邏輯，我們開始關心一段敘述如何組成。

從一般語言敘述的構成來看，如果我們不照慣例，而把所有的東西都說得清清楚楚的話，照理來說一段敘述應該是 "主詞+動詞+受詞"、"主詞+動詞"、"主詞+動詞謂語+修飾詞"的主要架構，配上動詞、主詞和受詞的修飾語或修飾子句構成的。但數學關心的，只是一個對象有怎麼樣的狀態，則另一個對象會有怎樣的狀態，也就是"主詞+動詞謂語+修飾詞"的架構配上推理的關係。描述狀態不外乎辨識特徵，事實上跟定義"集合"的本質，也就是辨別一個群體的共通性做的事是一樣的。

一段敘述都有它敘述的對象；比如說「業界(**有人**)對這個產品有興趣」、「(**所有**)外國旅客入境前都要防疫隔離」；邏輯學上，"**有人**"(更一般的說**存在一個人**)跟"**所有人**"(注意到所有外國旅客是**不是本國籍且身在我國**的所有人的略語)這兩個表述敘述對象範圍的詞語被稱為**量詞**(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)，這個簡記是非常直觀的。