User:C44986054/數理邏輯/一階邏輯
本篇是數理邏輯的第三章
基本符號
簡介
不同於命題邏輯，自一階邏輯，我們開始關心一段敘述如何組成。
從一般語言敘述的構成來看，如果我們不照慣例，而把所有的東西都說得清清楚楚的話，照理來說一段敘述應該是 "主詞+動詞+受詞"、"主詞+動詞"、"主詞+動詞謂語+修飾詞"的主要架構，配上動詞、主詞和受詞的修飾語或修飾子句構成的。但數學關心的，只是一個對象有怎麼樣的狀態，則另一個對象會有怎樣的狀態，也就是"主詞+動詞謂語+修飾詞"的架構配上推理的關係。描述狀態不外乎辨識特徵，事實上跟定義"集合"的本質，也就是辨別一個群體的共通性做的事是一樣的。
一段敘述都有它敘述的對象；比如說「業界(有人)對這個產品有興趣」、「(所有)外國旅客入境前都要防疫隔離」；邏輯學上，"有人"(更一般的說存在一個人)跟"所有人"(注意到所有外國旅客是不是本國籍且身在我國的所有人的略語)這兩個表述敘述對象範圍的詞語被稱為量詞(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)：
$\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$這樣的對應。
如此一來我們就有一套解釋一階邏輯語意的要素：
一個一階邏輯的解釋(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$的對應，所以序列也是一個函數；所以也是一個關係，從而更能看成一個二元有序對的集合)
項的解釋
所有變數的取值是${\{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$解釋：
$\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$下的"真假"：
(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)
甚至一些合式公式是不隨解釋的選取而總是為真，也就是說，他在"邏輯上"就是正確的
如果對於任何解釋$\displaystyle M$，${\models}_{M}\mathcal{B}$，稱$\mathcal{B}$為邏輯上有效的(logically valid)。反之對於任何解釋都為假的$\mathcal{B}$稱為邏輯上無效的(logically invalid)或是直稱矛盾。
一階邏輯形式理論裡的邏輯定理，依照我的們的期望理當是邏輯上有效的$\displaystyle wf$。其實一階邏輯的邏輯上有效，就是仿造命題邏輯的恆等式定義的。
類似的，我們也可以定義邏輯上等價和邏輯上推出：
對於合式公式$\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}$是邏輯上有效的)
重要的邏輯有效式
型式理論
(1)符號：
(a)量詞：$\forall$
(b)命題連接詞(propositional connectives)：$\neg,\Rightarrow$
(c)標點符號：逗號跟左右括弧。(但為了更方便閱讀命題連接詞施用的順序，我們會額外採用中括弧跟大括弧)
(d)一定要有，但最多跟跟自然數一樣多的變數符號。變數以小寫的任何西方語言字母代表(可能附有上下標或是prime)，如$a,\,\beta',\gamma_3,\,\delta^4,\,\aleph^5_5$
(e)可能有函數符號，可能有常數。但一定會有謂詞符號。這些符號都最多可以跟自然數一樣多。
- 另外，我們用大寫西方字母代表項，如$T,\,\Gamma$。
- 有時候謂詞符號和函數符號裡有大量的變數，為求簡便起見，我們以${\big{<}a_k\big{>}}^{n}_{k=1}$ 代表 $a_1,....,\,a_n$；而項亦採用這個方法，將$T_1,....,\,T_n$簡記為${\big{<}T_k\big{>}}^{n}_{k=1}$。
(2)合式公式($\displaystyle wf$)：
(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}'$。
(3)公理：
- $\displaystyle (a)$邏輯公理：如果$\mathcal{B},\mathcal{C},\mathcal{D}$是$\displaystyle wf$
(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)：根據不同理論的需求而訂製。
(4)推理規則：如果$\mathcal{B},\mathcal{C}$是$\displaystyle wf$，$\displaystyle x$是一個變數
MP律：$(\mathcal{B}\Rightarrow\mathcal{C})$跟$\mathcal{B}$可以推出$\mathcal{C}$。
其他的邏輯符號如下定義：
$\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})]$
而簡寫的規則，我們僅需將括弧規則裡第二項的施用順序改成
$\neg,\,\wedge,\,\vee,\,\forall,\,\Rightarrow,\,\Leftrightarrow$
注意到一階邏輯的形式理論，只要把原子公式視為命題邏輯形式理論裡的敘述字母，就可以完全引用之前的元定理。
(A4)是一切取代的最終極基礎。所以為了方便起見，套用(T)和(DN)以後，我們可以得到(A4)的"$\exists$"形式：
若於$\mathcal{B}(x)$，$T$對$x$是自由的，則
$\vdash\mathcal{B}(T)\Rightarrow(\exists x)\mathcal{B}(x)$
而應用這個定理的時候，我們一樣代稱為應用(A4)。
推廣律
公理(A7)可以稍加延伸，跟我們的直觀連繫在一起
元定理(定理的推廣律):
$\ulcorner\vdash\mathcal{B}\urcorner\to\ulcorner\vdash(\forall x)\mathcal{B}\urcorner$
| 證明 |
|---|
|
假設$\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$。 |
以下就是最一般情況的推廣律。
元定理($\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$
| 證明 |
|---|
|
我們對前提條件的數量$\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$。 |
GEN可以稍加修飾，以適合證明"$\exists$"形式的定理(以後簡稱 GENe)
元定理：
若$\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)和(A4)
並有以下直觀的選擇律
元定理($Rule\ C$, Rule of Choice, 選擇律)：
若$t$不曾出現在$\Gamma$和$\mathcal{A}(x)$裡，則
$\ulcorner\Gamma\vdash\mathcal{A}(t)\Rightarrow\mathcal{B}\urcorner$且$\ulcorner\Gamma\vdash(\exists x)\mathcal{A}(x)\urcorner$$\to$$\ulcorner\Gamma\vdash(\exists t)\mathcal{B}\urcorner$
| 證明 |
|---|
|
(1)$\mathcal{A}(t)\Rightarrow\mathcal{B}$ (Hyp) (2)$(\exists t)\mathcal{A}(t)\Rightarrow(\exists t)\mathcal{B}$ (GENe) (3)$(\forall t)[\neg\mathcal{A}(t)]\Rightarrow[\neg\mathcal{A}(x)]$ (A4) (4)$(\forall x)\{(\forall t)[\neg\mathcal{A}(t)]\Rightarrow[\neg\mathcal{A}(x)]\}$ (GEN) (5)$(\forall x)(\forall t)[\neg\mathcal{A}(t)]\Rightarrow(\forall x)[\neg\mathcal{A}(x)]$ (MP with 4, A7) (6)$(\forall t)[\neg\mathcal{A}(t)]\Rightarrow(\forall x)[\neg\mathcal{A}(x)]$ (MP with 5, A5) (7)$(\exists x)\mathcal{A}(x)\Rightarrow(\exists t)\mathcal{A}(t)$ (MP with 6, T) (8)$(\exists x)\mathcal{A}(x)\Rightarrow(\exists t)\mathcal{B}$ (D1 with 2, 7) 至此再套上MP律，定理就會得証$\Box$。 |
所以由推廣律，很容易證明以下關於"交換性"的定理
(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，都有一個數(也就是-a)，使a+(-a)=0"，但是任取一個a的數(-a)和任意的數b，b+(-a)並不一定會為零。
量詞表示的簡化
為了讓我們的敘述更好閱讀，對於變數$\displaystyle x_1,x_2,....,x_n$和任意變數$\displaystyle x,y$、合式公式$\mathcal{B}$、和可被簡記為$x\star y$，也就是只有$x$跟$y$完全自由的$\displaystyle A_{i}^{2}(x,y)$，我們定義：
$(\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且滿足....的話....則...."會不會不會跟上面的話簡化符號有所牴觸呢?為了回答這個問題，首先有以下定理：
(abb)$\vdash[\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})]\Leftrightarrow[(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}]$
| 證明 |
|---|
|
($\Rightarrow$) $\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})\vdash(\mathcal{A}\wedge\mathcal{B})\Rightarrow\mathcal{C}$ (1)$\neg(\mathcal{A}\Rightarrow\neg\mathcal{B})\Rightarrow\mathcal{C}$ (Hyp) (2)$\neg\mathcal{C}\Rightarrow(\mathcal{A}\Rightarrow\neg\mathcal{B})$ (MP with 1, T) (3)$(\neg\mathcal{C}\Rightarrow\mathcal{A})\Rightarrow(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})$ (MP with 2, A2) (4)$\mathcal{A}\Rightarrow(\neg\mathcal{C}\Rightarrow\mathcal{A})$ (A1) (5)$\mathcal{A}\Rightarrow(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})$ (D1 with 3, 4) (6)$(\neg\mathcal{C}\Rightarrow\neg\mathcal{B})\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$ (T) (7)$\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C})$ (D1 with 5, 6) ($\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}$。再由推論元定理就可以得證。 |
由此就可以證明以下定理($x\star y$代表$\displaystyle A_{i}^{2}(x,y)$；$x\ast y$代表$\displaystyle A_{j}^{2}(x,y)$)
$\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$中
| 證明 |
|---|
|
($\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) |
由以上的定理，可以歸納出更多變數狀況的簡化式，且簡化式前面的括弧可以"交換"的條件，是括弧中的項不能出現別的括弧裡的變數。
更一般來說，仿照上面的證明，定理可以延伸為
$\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$"得出類似的定理
$(\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$為此形式理論的定理：
(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)組合起來，很自然的確保"有人一定會跟指定數相等"：
$\vdash(\forall x)(\exists y)(x=y)$
等號的性質
(I) $\vdash T=T$
證明提示：(II) $\vdash (T=S)\Rightarrow(S=T)$
| 證明 |
|---|
|
(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$ |
(III) $\vdash (T=S)\Rightarrow[(S=R)\Rightarrow(T=R)]$
| 證明 |
|---|
|
(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$ |
(E2)的等價條件
元定理：
(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)$有
- $x=y\vdash f_i^n(a,....,x,....,b) = f_i^n(a,....,y,....,b)$($\displaystyle x$和$\displaystyle y$擺在同個順位上)
| 證明 |
|---|
|
從(E2)推理出兩點是很顯然的，因為(1)是(E2)的特殊情況；而(2)只不過是(E2)的特殊狀況套用(D2)而已。 現在我們從這兩點推出一般狀況的(E2)。 (I)擴張到有含常數的原子公式
(II)擴張到含函數符號的原子公式
(III)一般$\displaystyle wf$的情況
最後，雖然我們以上證明的都是取代一次的狀況，但是取代$\displaystyle n$次的情況，可以視為被取代$\displaystyle n-1$次的情況再取代一次；所以我們可以用取代一次的情況歸納到任意數量的取代，故(1)、(2)的要求和(E2)是等價的$\Box$ |
特別注意到如果把$x=y$換成某個符合(E1)、(E2)，$x$和$y$完全自由的$\mathcal{E}(x,\,y)$，也就是以$wf$而不是謂詞符號為基礎來定義"等號"的話，以上的定理和元定理還是會成立的。這是因為要求$x$和$y$在$wf$完全自由時確保了以(A4)進行代換時，得到和謂詞符號完全同樣的結果。
比如說，集合論就是以"屬於$x$等價於屬於$y$"去定義"x等於y"。
唯一性
$(\exists! x)\mathcal{B}(x):=(\exists x)\mathcal{B}(x)\wedge(\forall x)(\forall y)\{[\mathcal{B}(x)\wedge\mathcal{B}(y)]\Rightarrow (x=y)\}$
其中$\displaystyle y$是不出現在$\mathcal{B}(x)$的變數；$\displaystyle \mathcal{B}(y)$是來自於$\mathcal{B}(x)$中自由的$\displaystyle x$都被取代為$\displaystyle y$。
函數符號與唯一性
數學理論常常隨著內容的推進，而需要符號上的簡化；也就是一套型式理論增加新的符號(函數符號、常數符號)以後，我們仍然希望這個"新"型式理論和原來的型式理論，有同等的效力。具體來說，對每個新系統裡的合式公式$\displaystyle\mathcal{B}$，有一個符號上的變換，將$\displaystyle\mathcal{B}$轉變為原來系統中的合式公式$\displaystyle\mathcal{B}'$，並滿足
(1)$\displaystyle\mathcal{B}$在舊理論內的話，$\displaystyle\mathcal{B}'$就是$\displaystyle\mathcal{B}$。
(2)$\vdash_2\mathcal{B}\Leftrightarrow\mathcal{B}'$
(3)$\ulcorner\,\vdash_2\mathcal{B}\,\urcorner\to\ulcorner\,\vdash_1\mathcal{B}'\,\urcorner$
其中，$\vdash_1$代表舊理論內可以推出；$\vdash_2$代表新理論內可以推出。
讀者請自己檢驗，由(2)可以推出$\ulcorner\,\vdash_1\mathcal{B}'\,\urcorner\to\ulcorner\,\vdash_2\mathcal{B}\,\urcorner$，於是達到了一開始"效力等同"的要求!
直觀的動機
"相反數"的存在是仰賴於一個事實──"存在一個唯一的數，和原來的數相加為零"；所以一般來說，如果舊理論可以證明$(\exists!x)\mathcal{B}(a_1,\,....,a_n,\,x)$，那直觀上，可以用$\mathcal{B}[a_1,\,....,\,a_n,\,f^{n}_i(a_1,\,....,\,a_n)]$去"定義"一個新的函數符號$f^{n}_i$，去構成一個新的理論。(注意到如果沒有$a_k$的話，函數符號就會"退化"成常數)
那新舊理論的$\displaystyle wfs$間要如何做符號轉換呢?比如說，"相反數小於零"這個敘述明顯是新理論裡的敘述；那在舊理論，會把它敘述成"存在一個數，跟原來的數相加起來為零且這個數小於零。所以一般來說，如果在新理論裡有形如$\mathcal{C}[....,\,f(T_1,\,....,\,T_n),....]$的$\displaystyle wf$，那在舊理論裡，我們應該把它寫成$(\exists x)[\mathcal{C}(....,\,x,\,....)\wedge\mathcal{B}(T_1,\,....,T_n,\,x)]$。(注意到不管是新舊理論，相反數唯一性存在性都是個定理)
一個唯一性的定理
以嚴謹的方式實踐我們的動機前，需要一個輔助定理
$(\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)
| 證明 |
|---|
|
假設$t$不曾在$\mathcal{B}(x)$和$\mathcal{C}(x)$出現。 ($\Rightarrow$)
($\Leftarrow$)
|
新理論的假設
依照一開始的動機，新理論和舊理論都會滿足
$(\exists!x)\mathcal{B}(a_1,\,....,a_n,\,x)$ (U')
其中$\big<a_k\big>^{n}_{k=1}$和$x$在$\mathcal{B}$裡是完全自由的。(如此才能以A4與E2進行完全的代換)
但新理論加入了新的函數符號$f^{n}_i$，也就是加入了新公理
$\mathcal{B}[a_1,\,....,a_n,\,f^{n}_i(a_1,\,....,\,a_n)]$ (U)
注意到所有的公理形式都必須和$f^{n}_i$相容，特別是(A4)這個唯一描述項代換的公理。
新理論理當也要是套帶等號的形式理論。為此，考慮到(E2)的等價條件必須假設
$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$取代)
由此就可以得到新理論下
$\vdash_2 [x=f^{n}_i(a_1,\,....,\,a_n)]\Leftrightarrow\mathcal{B}(a_1,\,....,a_n,\, x)$ (E)
| 證明 |
|---|
|
($\Rightarrow$)
($\Leftarrow$)
|
所以(E)證實了我們的"直觀幻想"，跟"函數值"相等的敘述完全可以用$\mathcal{B}$替代。
符號變換
為了證明新舊理論效力等價的條件(2)；我們需要以下定理
$t$在新理論的$\mathcal{A}(t)$裡是完全自由的。新理論裡的項${\big{<}S_k\big{>}}^{n}_{k=1}$全部不含變數$x$，那
$\vdash_2 \mathcal{A}\big{[}f^{n}_i({\big{<}S_k\big{>}}^{n}_{k=1})\big{]}\Leftrightarrow(\exists x)\big{[}\mathcal{B}\big{(}{\big{<}S_k\big{>}}^{n}_{k=1},\,x\big{)}\wedge \mathcal{A}(x)\big{]}$
證明提示：
($\Rightarrow$)套用(A4)和(U)
($\Leftarrow$)套用上面的(aux)，然後用(A4)代換
這樣我們就可以對$f^{n}_i$在原子公式裡的數量做歸納，(然後配上GENe)而得出符合條件(2)的符號變換
(1) ${\{A^{m}_j[x_1,....,\,f^{n}_i({\big{<}a_k\big{>}}^{n}_{k=1}),....,\, x_m]\}}^{\prime}\asymp(\exists t)\{A^{m}_j[x_1,....,\,t,....,\, x_m]\wedge\mathcal{B}({\big{<}a_k\big{>}}^{n}_{k=1},\,t)\}$
(2)若$x$於$\mathcal{A}(x)$完全自由，則
- ${\{\mathcal{A}[f^{n}_i({\big{<}S_k\big{>}}^{n}_{k=1})]\}}^{\prime}\asymp(\exists t)\{{[\mathcal{A}(t)]}^{\prime}\wedge{[\mathcal{B}({\big{<}S_k\big{>}}^{n}_{k=1},\,t)]}^{\prime}\}$
注意以上的$t$都必須於變換時首次出現
注意上面的規則(2)可以透過以下的定理，把從變換產生的新量詞，遞迴地提到最外面
$t$和$s$在新理論的$\mathcal{A}(s,\,t)$裡是完全自由的。新理論裡的項${\big{<}T_k\big{>}}^{m}_{k=1}$和${\big{<}S_k\big{>}}^{n}_{k=1}$都不含變數$x$和$y$，那
$\vdash_2 \mathcal{A}\big{[}f^{n}_i({\big{<}T_k\big{>}}^{m}_{k=1}),\,f^{n}_i({\big{<}S_k\big{>}}^{m}_{k=1})\big{]}\Leftrightarrow(\exists x)(\exists y)[\mathcal{A}(x,\,y)\wedge\mathcal{B}({\big{<}T_k\big{>}}^{m}_{k=1},\,x)\wedge\mathcal{B}({\big{<}S_k\big{>}}^{m}_{k=1},\,y)]$
證明提示：套用(A4)、(U)和(aux)
一般的$wf$只要對$\neg$和$\Rightarrow$的數量做歸納，就會得到
(1)${(\neg\mathcal{A})}^{\prime}\asymp\neg{\mathcal{A}}^{\prime}$
(2)${(\mathcal{A}\Rightarrow\mathcal{C})}^{\prime}\asymp{\mathcal{A}}^{\prime}\Rightarrow{\mathcal{C}}^{\prime}$
(3)${(\forall x\mathcal{A})}^{\prime}\asymp\forall x{\mathcal{A}}^{\prime}$
如此就可以得到一般$wf$下的條件(2)。