# 形式理論

## 元邏輯
研究一個邏輯系統，好比一個語言學家研究英文的文法跟規則，他需要其他語言來當一個客觀的參照，避免陷入自己解釋自己的矛盾循環中。我們要研究的邏輯語言稱為**目標語言**(object language)，研究邏輯系統時，用來客觀參照目標語言的語言稱為**元語言**(metalanguage)，元語言的邏輯也會稱為**元邏輯**(metalogic)。而在元邏輯下，推出目標語言的有關性質特稱為**元定理**(metatheorem)。

事實上我們採用的元語言只是比較有條理的中文，配上一些邏輯符號:
:::success
(1)$\displaystyle \to$：實質條件意義下的推理

(2)$\ulcorner$, $\urcorner$：引用一段目標語言的敘述

:"「他是醫生」這句話是肯定句"，和"他是醫生"有使用上的差別，元語言的引號就跟前者代表**引用這句話並做語言學的說明**是一樣的，但後者是**單純的使用這句話**。

(3) $\displaystyle\sim$：否定後面的敘述。
:::
我們用中文的"或"跟"且"來代表元邏輯理的對應概念。我們也會使用中文語法裡的否定去否定一段元邏輯的敘述。

## 形式理論的要求
**所謂的推理一定是基於某些已知，運用某些推理規則而推出一個結果**，這就是數理邏輯理解證明所依據的哲學，所以這邊不會討論如哲學家康德(Immanuel Kant)所相信的**先驗**(a priori)或是自美國文學界興起的**超驗**(Transcendentalism)。

數學的終極目標就是找出讓某個現象成立**最少所需要的條件**(最好能互相獨立)，據以做為某套理論的基石，稱為**公理**(axiom)；但是有時候，套用一個理論解釋某個現象，像是用馬克士威的方程式去解釋電磁場在導線裡的傳播時，我們要額外考慮導線的截面是方形還是圓，這就是不在公理的範圍裡的**前提假設**(premise)。

由這些想法，就可以先粗略的給出數學理論在形式上要滿足的要求:
:::success
(1)有一套**符號**作為這個理論語言的單元，而這一套符號的數量可能跟[[自然數]]一樣多。任何一組符號稱為**公式**(formulas)

(2)有一套**文法**去規定，怎樣的符號組合是**合於這個理論的形式**而有意義的，符合規則的公式稱為**合式公式**(well-formed formulas)，簡記為$\displaystyle wf$，複數的時候加$\displaystyle s$。

(3)有一套$\displaystyle wfs$稱為**公理**(axiom)。

(4)一套推理規則。
:::
符合這些要求的數學理論稱為**形式理論**(formal theory)
:::success
ex.命題邏輯的形式理論

(1)$A_1,A_2,A_3....$採用當敘述字母；沒有下標的大寫英文字母用來表示任意的敘述字母；$\neg,\Rightarrow$採用當命題連接詞； " $($ " 與 " $)$ " 被用來表示命題連接詞的施用順序。

(2)敘述字母都是$wf$；如果$\mathcal{B},\mathcal{C}$是$wf$，那$(\mathcal{B})$、$\neg\mathcal{B}$與 $\mathcal{B}\Rightarrow\mathcal{C}$都是$wf$。除此之外沒有其他方法建構出$wf$。

(3)如果$\mathcal{B},\mathcal{C},\mathcal{D}$是$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}]$(反證法的一種形式)

(4)推理規則：$(\mathcal{B}\Rightarrow\mathcal{C})$跟$\mathcal{B}$可以推出$\mathcal{C}$(MP律)
:::

關於命題邏輯的形式理論，我們有幾項評注和額外的符號規定：

括弧可以依照命題邏輯裡敘述的括弧規則來省略；小括弧太多的話，會額外採用中括弧跟大括弧以分辨順序。

我們定義$\displaystyle wf$的方式是用**遞迴**的方式，也就是以敘述字母為基礎，一步步添加命題連接詞建構出來的。習慣上用草寫英文字母代表$wf$。

注意我們描述公理是以任意$wf$而非敘述字母為基礎，導致實質上有無限多條公理。這種定義方法稱為**公理形式**(axiom schema)

## 證明

形式理論中的$\mathcal{B}$的**證明**，指的是一列$wfs$

:::success
$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$
:::
滿足
:::success
1. $\mathcal{C}_n$必須是$\mathcal{B}$。
2. $\mathcal{C}_1$是前提假設或是公理。
3. $k>2$的話，除$\mathcal{C}_k$可能是前提假設或公理外，也有可能存在$\mathcal{C}_{l}$和$\mathcal{C}_{m}$ (其中$l, m < k$)，使$\mathcal{C}_{m}$就是$\mathcal{C}_{l}\Rightarrow\mathcal{C}_{k}$(也就是可以用MP律組合兩者而推出$\mathcal{C}_k$)
:::

:::success
ex.

命題邏輯的形式理論下，如果$\mathcal{B}$是$\displaystyle wf$，$\mathcal{B}\Rightarrow\mathcal{B}$的證明：

$\mathcal{C}_1$：$\{\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)

$\mathcal{C}_2$：$\mathcal{B}\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{B})\Rightarrow\mathcal{B}]$ (公理A1)

$\mathcal{C}_3$：$\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})$ (公理A1)

$\mathcal{C}_4$：$[\mathcal{B}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})]\Rightarrow(\mathcal{B}\Rightarrow\mathcal{B})$ ($\mathcal{C}_1$和$\mathcal{C}_2$加上MP律)

$\mathcal{C}_5$：$\mathcal{B}\Rightarrow\mathcal{B}$ ($\mathcal{C}_4$和$\mathcal{C}_3$加上MP律)
:::
證明所需的一群$\displaystyle wfs$，可以用$\displaystyle\Gamma$簡寫；$\mathcal{B}$在形式理論$\mathcal{L}$有證明；而這個證明裡或許有引用$\displaystyle\Gamma$裡的$\displaystyle wf$，或是引用$\mathcal{D}_1,\mathcal{D}_2,....,\mathcal{D}_k$裡的$\displaystyle wf$話，這種情況以$\Gamma,\mathcal{D}_1,\mathcal{D}_2,....,\mathcal{D}_k\,{\vdash}_{\mathcal{L}}\,\mathcal{B}$代表。**不需要的$wf$可以省略不寫。**

如果$\mathcal{B}$在$\mathcal{L}$的證明只需要公理，$\mathcal{B}$被稱為**定理**(theorem)，以${\vdash}_{\mathcal{L}}\,\mathcal{B}$代表。

定理可依據作者的觀感，將重要性比較小的別稱為**命題**(proposition)或是**性質**(property)；或為前面定理的直截結果而別稱為**系理**(corollary)或**引理**(lemma)。

如果很清楚採用哪個形式理論的話，${\vdash}_{\mathcal{L}}$的下標$\mathcal{L}$可以省略，像**本章採用的形式理論都是命題邏輯**，所以都省略。

## 推論元定理
在進一步說明形式理論的一些額外要求之前，需要了解一些命題邏輯的性質。

:::success
**推論元定理**(metatheorem of deduction)：

$\ulcorner\,\Gamma,\mathcal{B}\vdash\mathcal{C}\,\urcorner\to\ulcorner\,\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\,\urcorner$

**證明**(注意這是元邏輯意義下的證明)：
<details>

假設$\mathcal{C}_1,\mathcal{C}_2,....,\mathcal{C}_n$就是條件所說$\mathcal{C}$的證明，如果$\mathcal{C}_1$本身是從$\displaystyle\Gamma$來的前提假設或是公理，那根據公理(A1)，$\vdash\mathcal{C}_1\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}_1)$，所以由MP律$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_1$。

如果$\mathcal{C}_1$本身是$\mathcal{B}$，那根據我們講解證明的例子($\vdash\mathcal{B}\Rightarrow\mathcal{B}$)，仍然可以推出$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_1$，所以$\mathcal{C}_1$的情況已經全部證明完畢。

接下來我們要用歸納法；假設對$\displaystyle i<k$都有$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_i$。如果$\mathcal{C}_k$是公理、或是從$\displaystyle\Gamma$來的、或是他自己根本就是$\mathcal{B}$，仿造$\mathcal{C}_1$的情況就可以證明$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_k$。

剩下沒考慮的狀況是由MP律組合出$\mathcal{C}_k$的狀況，也就是有$\displaystyle l,m<k$使得

$\mathcal{C}_m:\mathcal{C}_l\Rightarrow\mathcal{C}_k$。

套用公理A2有

$\vdash[\mathcal{B}\Rightarrow(\mathcal{C}_l\Rightarrow\mathcal{C}_k)]\Rightarrow[(\mathcal{B}\Rightarrow\mathcal{C}_l)\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}_k)]$

套用我們歸納法的假設，加上MP律，就會發現$\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}_k$。這樣就可以一路歸納到$\mathcal{C}_n$也就是$\mathcal{C}$的情況，所以元定理得到證明。$\Box$

</details>
:::

這個元定理說"$\Rightarrow$"跟"$\vdash$"可以互換；因為$\ulcorner\,\Gamma\vdash\mathcal{B}\Rightarrow\mathcal{C}\,\urcorner\to\ulcorner\,\Gamma,\mathcal{B}\vdash\mathcal{C}\,\urcorner$是很顯然的，就只是MP律的應用而已。

有時會為了保持證明的"純潔"，不用申明採用推論元定理，我們會偷懶的把定理表達成$\mathcal{A}\vdash\mathcal{B}$的樣子，甚至以此類推，把$\Rightarrow$前的$\displaystyle wf$逐一的移到$\vdash$前以方便直觀的理解。

注意到推論元定理的證明僅僅需要MP律、(A1)和(A2)(所以日後可以直接適用於**一階邏輯**)。

由推論元定理配上MP律，可以很輕易得到以下很直觀的邏輯定理
:::success
$\displaystyle (D1)$$\mathcal{A}\Rightarrow\mathcal{B},\mathcal{B}\Rightarrow\mathcal{C}\vdash\mathcal{A}\Rightarrow\mathcal{C}$

$\displaystyle (D2)$$\mathcal{A}\Rightarrow(\mathcal{B}\Rightarrow\mathcal{C}),\mathcal{B}\vdash\mathcal{A}\Rightarrow\mathcal{C}$
:::

## 自洽性
本節會用到一些[常用的邏輯定理](/ll0Tu7mqTDSl2acTff_lhQ?view)，請依照定理的代號查找。

提出命題邏輯的形式理論以後，會很自然地會要求，**以真假值為基礎的命題邏輯下的恆等式，理當是這個形式理論下的定理**，反過來也要對。

讀者回憶一下命題邏輯曾證明的MP律；然後自證(A1)~(A3)都是恆等式，這樣就可以證明形式理論下的定理都是恆等式。

在證明恆等式都是命題邏輯形式理論的定理之前，我們需要一個輔助的元定理
:::success
**元定理**：

$\mathcal{A}$是一個含敘述字母$\displaystyle A_1,A_2,....,A_n$的$\displaystyle wf$；若根據某組指定的敘述字母真假值，得出的$\mathcal{A}$真假值下，做以下的選取

$A_k':
\begin{cases}
\begin{matrix}
A_k & (A_k:\top) \\
\neg A_k & (A_k:\bot)
\end{matrix}
\end{cases}$ $\mathcal{A}':
\begin{cases}
\begin{matrix}
\mathcal{A}& (\mathcal{A}:\top) \\
\neg\mathcal{A} & (\mathcal{A}:\bot)
\end{matrix}
\end{cases}$

則在形式理論下$A_1',A_2',....,A_n'\vdash\mathcal{A}'$

**證明**

<details>

$\displaystyle wf$是以$\Rightarrow$、$\neg$和敘述字母基礎，用**遞迴**的方式建構出來的，所以我們針對兩者的總數量做歸納，就可以遍及一切$\mathcal{A}$的可能形式。

數量為零的情況，$\mathcal{A}$就只是敘述字母，顯然本元定理是成立的。

現在假設$\Rightarrow$和$\neg$的數量少於$\displaystyle n$的情況，元定理是正確的；若$\mathcal{A}$內含有數量$\displaystyle n$個的$\Rightarrow$或$\neg$，則根據我們對$\displaystyle wf$的定義，這裡會有$\Rightarrow$和$\neg$的總數量少於$\displaystyle n$的$\mathcal{B}$和$\mathcal{C}$，使得$\mathcal{A}$可以表達成$\neg\mathcal{B}$或$\mathcal{B}\Rightarrow\mathcal{C}$這兩種可能的形式。

(1)$\mathcal{A}:\neg\mathcal{B}$

: 這種情況下，歸納法的假設可以寫為$A_1',A_2',....,A_n'\vdash\mathcal{B}'$。

: (1-a)$\mathcal{B}'$取為$\mathcal{B}$的時候("真")，那$\mathcal{A}':\neg(\neg\mathcal{B})$。則根據(DN)

: $\mathcal{B}\vdash\neg\neg\mathcal{B}$

: 故元定理成立。

: (1-b)$\mathcal{B}'$取為$\neg\mathcal{B}$的時候("假")，那$\mathcal{A}':\neg\mathcal{B}$。則根據(I)

: $\neg\mathcal{B}\vdash\neg\mathcal{B}$

: 故元定理成立。

: 故情況(1)下我們由少於$\displaystyle n$歸納到$\displaystyle n$的情況。

(2)$\mathcal{A}:\mathcal{B}\Rightarrow\mathcal{C}$

: 這種情況下，歸納法的假設可寫為$A_1',A_2',....,A_i'\vdash\mathcal{B}'$且$A_1',A_2',....,A_j'\vdash\mathcal{C}'$。($\displaystyle i,j<n$，注意這意思是合併兩者，正好是$\displaystyle n$個相異敘述字母)

: (2-a)$\mathcal{B}'$取為$\mathcal{B}$；$\mathcal{C}'$取為$\mathcal{C}$，那$\mathcal{A}':\mathcal{B}\Rightarrow\mathcal{C}$，那根據(A1)

: $\mathcal{C}\vdash\mathcal{B}\Rightarrow\mathcal{C}$

: 將$\displaystyle A_1',A_2',....,A_i'$和$\displaystyle A_1',A_2',....,A_j'$合併在一起當前置條件(**注意是它們的取法導致$\mathcal{B}'$和$\mathcal{C}'$的取法**)，故元定理成立。

: (2-b)$\mathcal{B}'$取為$\neg\mathcal{B}$；$\mathcal{C}'$取為$\neg\mathcal{C}$，那$\mathcal{A}':\mathcal{B}\Rightarrow\mathcal{C}$，那根據(M0)

: $\neg\mathcal{B}\vdash\mathcal{B}\Rightarrow\mathcal{C}$

: 故元定理成立。

: (2-c)$\mathcal{B}'$取為$\neg\mathcal{B}$；$\mathcal{C}'$取為$\mathcal{C}$，那$\mathcal{A}':\mathcal{B}\Rightarrow\mathcal{C}$，那同上根據(M0)，元定理成立。

: (2-d)$\mathcal{B}'$取為$\mathcal{B}$；$\mathcal{C}'$取為$\neg\mathcal{C}$，那$\mathcal{A}':\neg(\mathcal{B}\Rightarrow\mathcal{C})$，那根據(M1)

: $\mathcal{B},\neg\mathcal{C}\vdash\neg(\mathcal{B}\Rightarrow\mathcal{C})$

: 故元定理成立。

: 故(2)的狀況的確可以歸納到$\displaystyle n$。

綜上所述，元定理已對所有可能的$\mathcal{A}$形式完成證明$\Box$

</details>

例子：

$\mathcal{A}:\neg(\neg A_1\Rightarrow A_2)$，若指定$\displaystyle A_1$和$\displaystyle A_2$都為真，則會得到$\mathcal{A}$為假，這種情況下$\displaystyle A_1'$僅僅是$\displaystyle A_1$；$\displaystyle A_2'$僅僅是$\displaystyle A_2$，$\mathcal{A}'$為$\neg\neg(\neg A_1\Rightarrow A_2)$，則

$A_1,A_2\vdash\neg\neg(\neg A_1\Rightarrow A_2)$ (A1, DN)
:::
這個元定理非常的直觀；也就是沒有加上"$\neg$"可以視為形式理論的"真"，反之視為"假"，這樣的"真假組合"的確可以推出跟真假值相符合的"真值函數"。
:::success
**元定理**：(命題邏輯形式理論的完備性)

命題邏輯的真假值的恆等式也一定是命題邏輯形式理論裡的定理

**證明**

<details>

假設$\mathcal{A}$是含敘述字母$\displaystyle A_1,A_2,....,A_n$的$\displaystyle wf$，是真假值的意義下的恆等式，根據上面的元定理

$A_1',A_2',....,A_n\vdash\mathcal{A}$

$A_1',A_2',....,\neg A_n\vdash\mathcal{A}$

所以根據(A3')配上推論元定理

$A_1',A_2',....,A_{n-1}\vdash\mathcal{A}$

以這樣的手法消去，最後我們會得到$\vdash\mathcal{A}$。$\Box$

</details>
:::
真假值要求$\mathcal{A}$和$\neg\mathcal{A}$不能同時為真，所以兩者不可能同時為定理；一般來說，**一個$\mathcal{A}$和$\neg\mathcal{A}$不能同時為定理的形式理論**稱為**自洽的**(consistent)。更進一步的，回憶一下(M0)，這個定理的直觀意義是若有個$\displaystyle wf$他的否定跟本身都是對的，則可以推出任意$\displaystyle wf$是對的；這引申出自洽性更一般的定義，**一個並非所有$\displaystyle wf$都是定理的形式理論**稱為**絕對自洽的**(absolutely consistent)

## 公理的獨立性