語句邏輯的證明系統

 （這裡用的A、B、C可以替換成其他合法的語句）

證明系統裡有公理（axiom）和推論規則（rule of inference）這兩個部分。

Kiki上課時用的證明系統（PS系統）裡只用了兩個連接詞，¬和→。不過我忘記要怎麼證明這兩個連接詞就夠用了。另外，Kiki有提到其實只要「｜」這個連接詞^*1就夠用。證明系統的公理越少，以後在證明健全性和完備性時會比較簡單，但是做推論時會比較麻煩，要寫好幾行才能推論出想要的東西。

PS系統裡會用到「├」這個符號，如果我沒記錯的話這個符號的名字是single term style。

證明（proof）：├A
意思是A是公理，或A是由公理和推論規則產生的。A不需要任何前提就能堆論出來。

推導（deduction）：Γ├A
意思是A是由Γ這組前提，以及公理和推論規則產生的語句。Γ是由語句們形成的集合。當Γ├A裡的Γ是空集合時，它就是├A。

一致（consistency）：
Γ 是個一致的集合，若且唯若，對於某個語句A而言，不會有Γ├A而且Γ├¬A的情況發生。

PS系統的公理：

1. ├A→(B→A)
2. ├(A→(B→C))→((A→B)→(A→C))
3. ├(¬A→¬B)→(B→A)

PS系統的推論規則：Modus Ponens（MP）

• 由├A→B和├A可以得到├B，或者
• A→B, A├B

有了公理和推論規則後，就可以推論出其它定理（theorem）（因為還沒證明語句邏輯的健全性和完備性，所以不能用語句的真假值來證明這些定理）：

推導├A→A。

1. ├A→((A→A)→A)                                          公理1
2. ├(A→((A→A)→A))→((A→(A→A))→(A→A))   公理2
3. ├(A→(A→A))→(A→A)                                  1,2,MP
4. ├A→(A→A)                                                  公理1
5. ├A→A                                                          3,4,MP

推導Γ, A├B若且唯若Γ├A→B（這是後設定理，因為在語句邏輯的語法裡沒有說「Γ」、「若且唯若」是合法的語句邏輯符號）。

1.如果Γ├A→B則Γ, A├B。
當Γ├A→B時，如果在前提裡加進A，讓前提從Γ變成Γ, A，那麼除了
Γ, A├A→B以外我們還可以得到Γ, A├A。根據MP規則，從Γ, A├A→B和Γ, A├A我們可以推論出Γ, A├B。

2.如果Γ, A├B則Γ├A→B。
這時候要用到數學歸納法。用推導的長度為Γ, A├B的推導們排序（例如之前推導├A→A時推導的長度是五行）。

Base Case：
證明當Γ, A├B推導的長度是一行時，Γ, A├B則Γ├A→B會成立。

Γ, A├B推導的長度是一時，要嘛B和A是同一個語句，要嘛B是公理或Γ裡的某個語句。

1. B和A是同一個語句：
   那麼根據├A→A這個定理，Γ├A→B會成立。
2. B是公理：
   因此Γ├B。加上公理1Γ├B→(A→B)，使用MP規則可以得到Γ├A→B。
3. B是Γ裡的某個語句：
   因此Γ├B。加上公理1Γ├B→(A→B)，使用MP規則可以得到Γ├A→B。

Inductive Hypothesis：
假設當Γ, A├B的推導長度小於n時，Γ, A├B則Γ├A→B會成立。

Inductive Case：
利用Inductive Hypothesis證明當Γ, A├B推導的長度是n行時，Γ, A├B則Γ├A→B會成立。

Γ, A├B推導的長度是n時，要嘛B和A是同一個語句，要嘛B是公理或Γ裡的某個語句，要嘛B是用MP規則推論出來的。

1. B和A是同一個語句：證明方式和Base Case一樣。
2. B是公理：同上。
3. B是Γ裡的某個語句：同上。
4. B是用MP規則推論出來的：
   也就是說，B是這樣推論出來的：
   第1行：Γ, A├某個句子
   第2行：Γ, A├某個句子
   …
   第 i 行：Γ, A├C→B
   …
   第 j 行：Γ, A├C
   …
   第 n 行：Γ, A├B（根據第i行、第j行及MP）
   
   因為第 i 行和第 j 行的推論長度都小於第 n 行，所以它們都可以使用Inductive Hypothesis做推論。所以Γ, A├C→B使用IH後我們得到Γ├A→(C→B)。Γ, A├C使用IH後得到Γ├A→C。再使用公理2Γ├(A→(C→B))→((A→C)→(A→B))和MP規則，就可以得到Γ├A→B。
   

其他PS系統裡的後設定理（大概不只這些）：

• Idempotence：Γ, A├A
• Monotonicity（單調性）：如果Γ├A，那麼Γ, Σ├A
• Cut：如果Γ, A├B而且Γ, A, B, Σ├C，那麼Γ, A, Σ├C

其他PS系統裡的定理：

• →的傳遞性：A→B, B→C├A→C
• ├¬A→(A→B)
  如果某組前提可以推論出A也可以推論出¬A（也就是說，這組前提不一致），那麼根據MP規則及這個定理，這組前提可以推論出任何語句。
• ├¬¬A→A
• ├A→¬¬A
• ├A→((A→B)→B)
• ├(A→B)→(¬B→¬A)
• ├(A→¬A)→¬A
• 懶得列了，就這樣。有興趣的人可以試試看自己推導這些定理。不過我幾乎都證不出來，嘛哈。

參考資料：中正哲學所九十九學年度第一學期進階邏輯Kiki的講義。

Note：

1. 這個連接詞的真值表如下：
   A｜B
   T F T
   T T F
   F T T
   F T F