Re: [其他] 邏輯中的"定義"該怎麼寫？

[joshs (Josh Ko)]

處理「定義」最簡單的方式我想應該是先區分「後設語言」(meta-language) 和
「對象語言」(object language), 然後說「定義」是後設語言裡的機制，
目的是為了方便寫出對象語言裡常用或重要的樣式。

我自己的經驗是傳統數學裡很少談「型式」「語法」(syntax) 這類數學物件，
到了後設數學必須談這些了，傳統數學寫作風格卻又容易讓後設語言和
對象語言混雜在一起。相較之下，程式的本質是符號操作 (symbol/syntax
manipulation), 程式員的工作是撰寫（後設）符號以操作（對象）符號，
因此若有程式基礎，要區分後設語言和對象語言應該是很容易的。

以下我嘗試簡單介紹一下程式觀點，用的語言基本上是 Haskell:

  http://www.haskell.org

但符號上略作變動以利數學背景讀者理解，也不使用 Haskell 的完整語意。
前半段是 Haskell 簡介，後半段我用 Haskell 寫一點點命題邏輯，藉以說明
後設語言和對象語言之分別，以闡明上述「定義為後設語言裡的機制」之意思。

Haskell 程式是由「函式定義」構成，例如

  double : Int -> Int
  double x = x + x

  square : Int -> Int
  square x = x * x

這裡定義兩個函式 double 和 square, 它們都接收一個整數並算出另一個整數。
（注意 Haskell 語法上套用函式時不寫 double(x) 而只寫 double x, 但必要時
還是要加括號。欸，細節就不詳述了... 這篇的例子應該都可以看懂才是。）
Haskell 程式執行就只是把一個給定式子儘量化簡，遇到函式時參考其定義，
將等號左邊的樣式換成右邊的式子。例如 square (double 4) 的計算過程是

    square (double 4)
  = square (4 + 4)
  = square 8
  = 8 * 8
  = 64

（假設 '+' 和 '*' 的行為是我們熟悉的那樣）計算結果即為 64.
簡單地說：直接理解成數學上的代換就行了。

在 Haskell 裡面我們可以處理比 Int 更複雜的資料型態 (datatypes),
例如下面這行

  data IntList = Nil | Cons (Int × IntList)

定義了一個新的型態 IntList（想像成集合），裡面的元素是用

  Nil : IntList

和

  Cons : Int × IntList -> IntList

自由生成的。（Nil 本身就是個 IntList；Cons 接收一個 Int 和一個 IntList,
產出一個 IntList.）例如以下

  Nil
  Cons (0, Nil)
  Cons (0, Cons (1, Nil))
  Cons (0, Cons (1, Cons (2, Nil)))

都是 IntList 的元素（如同 0, 1, 2 都是 Int 的元素一般）。
如此定義的資料型態我們稱為「代數型態」(algebraic datatypes).

Haskell 提供一種機制「樣式匹配」(pattern matching) 讓我們在代數型態上定義函式。
例如，我們可以寫一個函式把某個 IntList 裡面所有的整數加起來：

  sum : IntList -> Int
  sum Nil            = 0
  sum (Cons (x, xs)) = x + sum xs

如此我們便指定當 sum 遇到 Nil 和 Cons 時應如何化簡。
因為 IntList 的元素只可能用 Nil 和 Cons 構造出來，有了以上兩條化簡規則，
sum 便對任何 IntList 都定義妥當（亦即對任何 IntList 都能確切算出一個 Int）。
例：

    sum (Cons (0, Cons (1, Nil)))
  = 0 + sum (Cons (1, Nil))
  = 0 + 1 + sum Nil
  = 0 + 1 + 0
  = 1

至此 Haskell 簡介結束。

接下來我們考慮命題邏輯語言最簡單、僅有「蘊含」的版本。
這語言在 Haskell 裡定義成

  data Prop = Var Int | Imp (Prop × Prop)

我們用 Prop 的元素表示「命題式」 (propositional formulae), 而且變數
直接以整數命名（而非常見的 P, Q, R, ... 之類的）。

例如

  Imp (Imp (Imp (Var 0, Var 1), Var 0), Var 0)

代表的是 Peirce's law, 對應的一般寫法是

  ((P => Q) => P) => P

（假設 P 對應於 0, Q 對應於 1.）
命題邏輯上可定義二值語意：令真假值之型態為

  data Bool = False | True

則命題式之真假值可如此定義：

  truth : (Int -> Bool) × Prop -> Bool
  truth (s, Var x)  =  s x
  truth (s, Imp (p, q)) | truth (s, p) == False  =  True
                        | otherwise              =  truth (s, q)

即：固定變數上的真假值（表示為一個 Int 到 Bool 的函式），給定一命題式，
此命題式只可能是變數或蘊含型式。第一個情況時，直接回傳賦予該變數之真假值；
第二個情況時，令前件為 p, 後件為 q, 若 p 的真假值為 False,
整個命題式之真假值即算為 True, 反之則算為 q 之真假值。

循此脈絡，可繼續以 Haskell 寫下命題邏輯其餘定義（然後證明定理）。
但至此我們已經可以試著理解後設語言和對象語言的分別：我們探討的「對象」
是命題邏輯的語言，而探討所用的（後設）語言是 Haskell. 命題邏輯語言
在 Haskell 裡面定義成一個資料型態（命題式之集合），其元素是以 Var 和
Imp 自由生成的樹狀結構，本質只是純粹的符號，而我們寫 Haskell 程式
來操作這些符號。傳統數理邏輯的後設語言和對象語言直覺上太過類似，從而
容易混淆兩種語言，改用 Haskell 的好處是後設語言和對象語言變得很容易區分
（前者是整個 Haskell, 後者只是用 Haskell 寫下的一個資料型態）。

最後我們回到一開始的問題：何謂定義？例如，定義 bi-implication P <=> Q 為
(P => Q) /\ (Q => P) 是什麼意思？假設我們擴充 Prop 的定義，多加一條
Conj (Prop × Prop) 代表 conjunction. 雙向蘊含在 Haskell 便寫為

  biImp : Prop × Prop -> Prop
  biImp (p, q) = Conj (Imp (p, q), Imp (q, p))

即：biImp (p, q) 是在後設語言裡對 Conj (Imp (p, q), Imp (q, p)) 的縮寫，
而不是對象語言內的構件。更進一步的定義可引用既有定義，但最終會全部
化簡（展開）為對象語言。一般說數學基礎是公理化集合論也是這個意思：
數學用的符號繁多，但這些（原則上）最終都可化簡（展開）為集合論的單純語言。

※ 引述《yueayase (scrya)》之銘言：
: 看了以上的討論, 我不知道type theory和邏輯符號語言之間的差別

Martin-Lof's type theory 可理解為表達能力極其豐富的程式語言或
具完整計算意義的數學基礎理論（包括高階邏輯）—「直構數學」
(intuitionistic mathematics) 的定理與證明可在 MLTT 內型式化，
並等價於真正能跑的程式。

這領域仍在火熱發展，如近年來由 Fields Medal 得主 Vladimir Voevodsky
領軍的 univalent foundations of mathematics

  http://uf-ias-2012.wikispaces.com

企圖將 homotopy theory 帶入 type theory, 打造數學的全新基礎。（不過我不熟...）

: 因為我也曾經看過像logic set and recursion(http://ppt.cc/PatL)之類的書
: 裡面主要就是在說邏輯符號系統的language structure是怎樣
: 怎樣去interpret這些language意思
: 像之前提到的 A Mathematical Introduction to Logic也是在說這些東西
: 就不是很清楚type theory和這類書籍所說的有什麼差別
: 附帶一提,
: 這些東西又好像和computer science 的 formal language(eg: context-free grammar)
: 或是 computation theory(eg: Turing machine <=> λ-calculus, decidability...)
: 有一些關聯
: 的確, 聽說作Artificial Intelligence的人, 早期好像也在研究logic...

是的，關聯密切。整個來龍去脈詳細要說清楚得花不少篇幅，所以直接打個廣告：
這些在「邏輯、語言、與計算」暑期研習營（的偶數年）會提到！課程教材都會上網，
例如去年的在這裡：

  http://flolac.iis.sinica.edu.tw/flolac12

--
感謝 xcycl 邀我下水以及審稿。

--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 86.2.123.53
推 xcycl       :幾句話拐到精彩好文 推
推 hcsoso      :推推 josh!
推 WINDHEAD    :
推 HmmHmm      :推 原來 Voevodsky 也做這個...
推 coolbetter33:這一篇文章值 1000 Ptt幣
推 laba1014    :好文!!!
推 suhorng     :這串厲害!
推 TassTW      :推推
→ t0444564    :作者只有六篇...
※ 編輯: joshs           來自: 86.2.123.53          (04/19 09:00)