啊啊哲學: 語句邏輯的健全性

如果你不太能理解這篇文章在幹嘛，建議先讀過下列文章。

健全性（soundness）：如果Γ├A，那麼Γ ⊧A。如果某組語句Γ可以推導出某個語句A，那麼不管語句們的真值設定是什麼，都不會出現Γ裡的語句都為真但A為假的情況（Γ可以是空集合）（健全性是後設定理）。

PS系統的健全性證明：

使用強數學歸納法，用推論出A需要幾行證明為Γ├A排序。

B.C.當證明行數為1的時候，A要嘛是公理，要嘛是前提。

A是公理：
1. 公理1：├A→(B→A)
  如果有個真值設定v讓v'(A→(B→A)) = 0（讓A→(B→A)為假），那麼v'(A) = 1而且v'(B→A) = 0。想讓v'(B→A) = 0，那麼v'(B) = 1而且v'(A) = 0。但是v'(A)在之前設定的值是1（畫底線的地方），所以找不到讓v'(A→(B→A)) = 0的真值設定。因此 ⊧A→(B→A)成立。
  .
2. 公理2：├(A→(B→C))→((A→B)→(A→C))
  如果有個真值設定v讓v'((A→(B→C))→((A→B)→(A→C))) = 0，那麼v'(A→(B→C)) = 1而且v'((A→B)→(A→C)) = 0。讓v'((A→B)→(A→C)) = 0，那麼v'(A→B) = 1而且v'(A→C) = 0。讓v'(A→C) = 0，那麼v'(A) = 1而且v'(C) = 0。v'(A) = 1，所以要讓v'(A→B) = 1的話，v'(B) = 1。但是v'(A) = 1而且v'(C) = 0而且v'(B) = 1的話，v'(A→(B→C)) = 0，和之前v'(A→(B→C)) 設定的值（畫底線處）不同。因此找不到讓v'((A→(B→C))→((A→B)→(A→C))) = 0的真值設定。⊧(A→(B→C))→((A→B)→(A→C))成立。
  .
3. 公理3：├(¬A→¬B)→(B→A)
  如果有個真值設定v讓v'((¬A→¬B)→(B→A)) = 0，那麼v'(¬A→¬B) = 1而且v'(B→A) = 0。讓v'(B→A) = 0，那麼v'(B) = 1而且v'(A) = 0。但是如此一來會讓v'(¬A→¬B) = 0，所以⊧(¬A→¬B)→(B→A)成立。
  .
A是前提：
當前提裡的所有語句φ在某個真值設定v底下，v'(φ) = 1，那麼v'(A)當然也會是1。

I.H.假設，當Γ├A的證明長度小於n時，如果Γ├A則Γ ⊧A。

I.C.當Γ├A的證明長度等於n時，A要嘛是公理，要嘛是前提，要嘛是用MP規則推論出來的。

A是公理的話，在B.C.已經證明公理都是恆真句了，所以Γ⊧A（Ａ是公理）。

A是前提的情況，證明方式和B.C.差不多。

A是用MP規則推論出來的，也就是說，Ａ是如下推論出來的：
第1行：Γ├某個句子
第2行：Γ├某個句子
…
第 i 行：Γ├B→A
…
第 j 行：Γ├B
…
第 n 行：Γ├A（根據第i行、第j行及MP）

因為第 i 行和第 j 行的推論長度都小於第 n 行，所以它們都可以使用I.H.做推論。所以可以得到Γ⊧B→A和Γ⊧B。Γ⊧B→A的意思是，在任何真值設定v下，如果有v'讓Γ裡所有語句的值都是1，那麼那個v'也會讓B→A的值是1（v'(B) = 0 或v'(A) = 1）。Γ⊧B的意思是，在任何真值設定v下，如果有v'讓Γ裡所有語句的值都是1，那麼那個v'也會讓B的值是1。

根據上一段畫了底線的那兩句話，可以知道，在Γ⊧B→A和Γ⊧B都成立的情況裡，
在任何真值設定v下，v'(A) = 1。因此，在Γ⊧B→A和Γ⊧B都成立的情況裡，Γ⊧A也成立。