把日常邏輯詞形式化#

卡羅爾（Lewis Carroll）的對話中，烏龜拒絕「正常使用」if-then 等日常用語。本章要做的是：設計一個形式系統，其中的符號被迫表現得像「and」、「if-then」、「or」、「not」應該表現的那樣。

僅依賴上述四個語詞正確用法的推理，稱為命題推理（propositional reasoning），相應的形式系統稱為命題演算（Propositional Calculus）。

符號表與第一條規則#

符號集合：

P, Q, R   （以及附加撇號的 P', Q', R', P'', ... 衍生原子）
∧  ∨  ⊃  ~        （and, or, if-then, not）
< >                 （分組符號，相當於括號）

為避免符號衝突，本書使用 ⊃（讀作「蘊含」、「if … then …」），符號 ~ 表示「not」。書中原文以 ƒ 代替 ⊃（fantasy / function）。

第一條規則：

合併規則（Joining）：若 x 與 y 都是定理，則 <x∧y> 也是定理。

良構字串#

良構字串以遞迴方式定義：

• 原子：P, Q, R, 以及附加撇號的版本，皆為良構
• 形成規則：若 x、y 為良構，則下列也都是良構：
  • ~x
  • <x∧y>
  • <x∨y>
  • <x⊃y>

判斷一個字串是否良構，可用「由上而下」的決策程序——把規則反向跑到底，最終必觸及原子。

其餘規則#

• 分離規則（Separation）：若 <x∧y> 是定理，則 x 與 y 也都是
• 雙波浪規則（Double-Tilde）：在任一定理中，~~ 可任意刪除或插入（前提是結果仍為良構）
• 對位規則（Contrapositive）：<x⊃y> 與 <~y⊃~x> 可互換
• 德摩根規則（De Morgan）：<~x∧~y> 與 ~<x∨y> 可互換
• 切換規則（Switcheroo）：<x∨y> 與 <~x⊃y> 可互換
• 分離（脫離）規則 / Modus Ponens：若 x 與 <x⊃y> 都是定理，則 y 也是

沒有公理：幻想規則#

命題演算沒有公理——所有定理都從一條特殊規則衍生：幻想規則（Fantasy Rule）。

幻想規則的操作：

[            ← push（進入幻想，用方括號標示）
  x          前提（fantasy 的開頭）
  ...        在幻想內推導
  y          幻想的結論
]            ← pop（離開幻想）
<x⊃y>        ← 真正的定理被寫出來

意義是：「假如 x 是定理，那麼 y 就是定理」——把這個觀察「裝進」系統內部，成為定理 <x⊃y>。

範例：

[
  P                premise
  ~~P              double-tilde
]
<P ⊃ ~~P>          fantasy rule

帶入規則：跨層級的有限通行證#

帶入規則（Carry-over）：在幻想內，可從外一層（更「真實」）取得任一定理使用。

但反向不通行——幻想內的定理不能輸出到外層，否則任何字串都可當前提，再被當作定理「私運」出來。

這就像「電影院內禁菸」的標示：實際上適用於電影中的角色，乃至電影中電影裡的角色——但反過來，電影裡的「禁菸」標示對戲外觀眾無效。

幻想可以巢狀#

[                       push outer
  P                     premise
  [                     push inner
    Q                   premise
    P                   carry-over from outer
    <P∧Q>              joining
  ]                     pop inner
  <Q ⊃ <P∧Q>>          fantasy
]                       pop outer
<P ⊃ <Q ⊃ <P∧Q>>>      fantasy

符號的詮釋#

∧  ↔  and（且）
∨  ↔  or（或，包含性「or」：x 或 y 或兩者）
⊃  ↔  implies / if-then（蘊含）
~  ↔  not（否定）
<,> ↔  群組符號，類似算式中的括號

原子（P、Q、R）可詮釋為任意一句句子（同一字串中重複出現須詮釋為同一句）。

一些禪味的例子#

把 P 詮釋為「此心是佛」，Q 詮釋為「此麻三斤」，則：

• <P ⊃ ~~P> 讀作：「若此心是佛，則並非此心不是佛。」
• <<P∧Q> ⊃ <Q∧P>> 讀作：「若此心是佛且此麻三斤，則此麻三斤且此心是佛。」

看似平庸，因為命題演算只能生成普世為真的陳述。它的功能不是揭露新真理，而是「機械地、不假思索地從真步向真」，像一個極度小心避免落入溪流的踏石人。

半詮釋與「公式式真理」#

把符號中除原子外都翻譯回中文，稱為半詮釋：

• <P∨~P> 的半詮釋是「P 或非 P」
• 無論 P 代入什麼，整句都為真

命題演算的核心特性：所有定理在半詮釋下都是普世為真的句子模式。

「岩頭斬猴」公案的形式化#

禪宗公案「岩頭斬猴」：

岩頭舉斧曰：「道得也斬卻汝頭，道不得也斬卻汝頭。」

設 P = 「你開口」，Q = 「我斬汝頭」，則岩頭的威脅可形式化為：

<<P ⊃ Q> ∧ <~P ⊃ Q>>

讀者可推導：在這個前提下，無論 P 真假，皆能推出 Q——「頭定要被斬」。命題演算僅花二十幾步即可導出 Q，最後使用的規則正是「分離（detachment）」。

公案本身的結局：兩僧繼續靜坐，岩頭放下斧頭說「你們是真正的禪修者」——但這已脫離形式系統能處理的範疇。

命題演算有決策程序嗎？#

命題演算的所有定理就是「在所有可想像世界都為真的陳述」。要問的是：

是否存在機械方法判定任意字串是否為定理？

是的——可用真值表（truth tables）作為決策程序。因此命題演算的定理集合不只是遞迴可枚舉，還是遞迴的。

那麼禪宗公案呢？能否設計一個「機械決策程序」分辨真公案與假公案？這是個開放性問題。

系統一致嗎？#

兩個立場辯論：

• 謹慎派（Prudence）：所有定理「在直覺詮釋下都為真」——這需要證明
• 不謹慎派（Imprudence）：規則就是直覺用法的編碼——若你信任自己的推理，就應信任這個系統。要求進一步證明，等於要求「比自己理智更高的可信度」

這正是卡羅爾對話的核心：你無法用邏輯證明邏輯。最終總會抵達一個必須以信任接受的層級——「我知道我是對的」。

推理系統像一顆雞蛋：你可以用越來越多層的盒子包裹它，但仍可想像某個變故能擊破它。最外層永遠是不可證的假設。

衍生規則與後設定理#

實際使用時，若已導出 <P∨~P>，便會「直接」使用 <Q∨~Q>——把舊定理當作「定理模式（theorem schema）」。這是衍生規則（derived rule）或後設定理（metatheorem）：

• 它在更高層談論系統，不屬於系統本身
• 對它的證明用「I-mode」直覺推理進行，不是形式推導

一旦你允許「為了便捷而跳出形式系統」，便破壞了形式系統的初衷——可機械化檢查每一步的嚴格性。

你可以把後設理論也形式化，再形式化後設後設理論……但永遠會有某個最頂層必須訴諸非形式直覺。

證明 vs. 推導#

• 證明（proof）：人類語言寫的、給人類看的非形式推理；每一步「感覺對」
• 推導（derivation）：每一步機械、明確、瑣碎，但整體可能極為冗長

兩種「簡單」是互補的：

證明簡單  →  每步直覺到位，但依賴複雜的人類語言
推導簡單  →  每步瑣碎到無可挑剔，但總步數天文數字

矛盾的兩種命運#

考慮以 <P∧~P> 為前提的幻想，推導出：

<<P∧~P> ⊃ Q>

由於 Q 可詮釋為任意句子，這意味著：

「從矛盾可推出任何事」（Ex contradictione quodlibet）。在基於命題演算的系統中，矛盾不會被局部限制，而會像癌細胞瞬間擴散到整個系統。

這顯然不像人類思考——當你發現自己的想法自相矛盾，你會去找出矛盾的源頭並修正，而非宣稱「現在我相信一切」。

緩解嘗試#

• 相關蘊含（relevant implication）（Anderson 與 Belnap 的《Entailment》）：限制規則的適用脈絡，要求 if-then 兩端真有因果或內容關聯
• 更激進的方向：放棄完備性與一致性，模仿人類含糊容錯的推理

命題演算的強項與弱點#

• 強項：簡單、精確、可機械化，能完美處理一階命題推理
• 弱點：缺乏量化（「所有」、「存在」），對矛盾過度敏感
• 可被嵌入更大的系統：下一章將把它整個納入排版數論（TNT），用於形式化數論推理