MU 謎題與形式系統

形式系統：本書的核心概念之一#

形式系統（formal system）是本書反覆出現的關鍵概念。本章使用的類型由美國邏輯學家艾米爾·波斯特（Emil Post）在 1920 年代發明，常稱為「波斯特生產系統」（Post production system）。為了讓讀者實際體會它的味道，作者拋出一則小謎題作為入門。

MU 謎題：你能從字串 MI 出發，依照下面四條規則，產生出字串 MU 嗎？

MIU 系統的元件#

MIU 系統只使用三個字母：M、I、U。所有「字串」（string）皆由這三個字母按固定順序排列而成。

公理（axiom）：唯一被「免費」給予的字串是 MI
推導規則（rules of inference 或 rules of production）：以下四條典型規則

規則 I:   若字串結尾是 I，可在尾端加上 U。
          例: MI → MIU

規則 II:  若擁有 Mx，可生成 Mxx（x 代表任意字串）。
          例: MIU → MIUIU；MUM → MUMUM

規則 III: 若字串中出現連續的 III，可將其替換為 U。
          例: UMIIIMU → UMUMU；MIIII → MIU 或 MUI

規則 IV:  若字串中出現 UU，可將其刪除。
          例: MUUUIII → MUIII

規則是單向的，不能反向使用。例如不能從 MU 倒推出 MIII。

定理、公理與推導#

凡是能由公理出發、循規則產生出來的字串，都稱為該形式系統的定理（theorem）。

此處的「定理」與日常用法不同。為了區別兩種意義，作者在書中採用大小寫慣例：
大寫 Theorem：一般意義上由邏輯論證證明為真的命題
小寫 theorem：技術意義上由規則機械式生成的字串

「推導」（derivation）則是逐行展示如何依規則產生某個定理。例如推導 MUIIU：

(1) MI                  公理
(2) MII                 對 (1) 套用規則 II
(3) MIII                對 (2) 套用規則 II
(4) MIIIIU              對 (3) 套用規則 I
(5) MUIU                對 (4) 套用規則 III
(6) MUIUUIU             對 (5) 套用規則 II
(7) MUIIU               對 (6) 套用規則 IV

推導（derivation）與證明（proof）的概念類似，但前者更為冷峻、純粹符號性。

系統之內與系統之外#

大多數人玩 MU 謎題時，會隨意生成一些定理，逐漸觀察到某些性質。例如：

所有定理的首字母都是 M
這是因為四條規則都不會改變首字母——可追溯到唯一的公理 MI

這個觀察點出了人類與機器的重要差別：

機器可以被設計為機械地不斷生成定理，卻永遠不察覺它在做什麼
人類幾乎不可能完全不察覺自己在做什麼——觀察與反思是人類意識的內建特性

兩種工作模式#

作者借此引出兩種模式（並湊齊 M、I、U 三個字母）：

M-mode（機械模式，Mechanical mode）：純粹依規則操作符號
I-mode（智能模式，Intelligent mode）：跳出來反思、找模式、嘗試非形式的捷徑
U-mode（無模式，Un-mode）：禪宗式的進路，將於後續章節展開

智能的一項內在特性，是能跳出當前任務、檢視自身所做之事——這就是「跳出系統」（jumping out of the system）。

例如：

讀書讀到累了會放下書去睡覺
看電視看到不滿意會轉台，更激進的人會直接把電視關掉
在西洋棋程式比賽中，一支弱小程式擁有「形勢無望時主動認輸」的功能，雖屢戰屢敗，卻被視為某種跳出系統的能力

決策程序#

MU 謎題還引出一個關鍵問題：如何判斷一個字串是不是定理？

天真的「測試」——「等到該字串被某個系統地枚舉定理的精靈生成出來，就知道它是定理」——並不令人滿意，因為它可能要等無限長的時間。

決策程序（decision procedure）：能在有限時間內判定任意字串是否為定理的程序，是形式系統的「litmus test」（試紙）。

兩種「刻畫定理集合」的方式對比：

隱式刻畫：規則與公理確實已隱含地定義了所有定理（與所有非定理）
顯式刻畫：決策程序提供具體、有限的判定方法

一個形式系統的公理集合本身必須有決策程序——必須能判斷任意字串是否為公理。但是「定理集合」未必有決策程序。

當你第一次面對 MIU 系統時，定理被隱式定義了，但 MU 是不是定理仍完全不清楚——這正是後續章節要逐步揭開的問題。

基本術語盤點#

本章引入了一整組形式系統的基本詞彙：

字串（string）：符號的有序排列
公理（axiom）：免費給予的起始字串
規則（rule of inference / production）：把字串變換為另一字串的操作
定理（theorem）：可由公理透過規則生成的字串
推導（derivation）：逐行記錄定理產生過程
形式系統（formal system）：以上元素的整體
決策程序（decision procedure）：判定定理身份的有限程序
在系統內 vs. 系統外（working inside/outside the system）：兩種思考模式