Set-theoretic inductive types

中午有人問到 structural induction 是不是一條 axiom，Max 的答案最為全面：系統外我們自然認為 induction 對，至於在系統內的話，first-order logic 必須要設成 axiom (scheme?)，到 FLOLAC '08 講的 second-order propositional logic（對應 polymorphic lambda-calculus）就可以用 Church encoding 表示自然數，從而自然地有 induction principle。我想的則是在型式系統的邊界處：在一般的數學架構下我們怎麼促成 induction？Category theory 用 initial F-algebra 弄得很漂亮，set theory 的話可以用 monotonic functions on sets + Knaster-Tarski Theorem 處理，都是把 inductive datatypes 定義得能夠做 induction。以下記錄第二種做法備查，因為我在回憶這種做法時有卡了一下 XD。

先在一個夠大的宇集裡隨便挑一個 constant z 和一個 injective "label" function s。（這句話有辦法說得更好嗎？或許用 axiom of infinity？）（不用假設 0 不在 s 的 range 裡面。直覺上，假設 0 = s (s 0') 而 0' 是我們心目中真正的零，那麼我們定出來的自然數集就是從二開始算。）在集合上定義一個 function f S := { 0 } ∪ { s x | x ∈ S } ，f 在 set inclusion 下是 monotonic，意思是 X ⊆ Y 時有 f X ⊆ f Y。根據 Knaster-Tarski Theorem，f 有 least fixed-point N，它也會是所有滿足 f X ⊆ X 的 set X 裡面最小的 — 若 X 滿足前式，則一定有 N ⊆ X。現在我們就把 N 當作自然數。假設我們有個性質 P x 要證明對 N 的所有元素成立，定義 X := { x | P x }，如果我們能夠證明 f X ⊆ X，即

  f X ⊆ X
⇔   { definition of f }
  { 0 } ∪ { s x | x ∈ X } ⊆ X
⇔   { since A ∪ B ⊆ C ⇔ A ⊆ C ∧ B ⊆ C }
  0 ∈ X ∧ (x ∈ X ⇒ s x ∈ X)

那麼我們就有 N ⊆ X，即 x ∈ N ⇒ x ∈ X，後件再用 P 改寫一下，就是 x ∈ N ⇒ P x。因此藉著如此定義 N，我們就免費得到 N 上的 induction principle 了。

--
寫這篇的時候也會卡，而且每次 monotonic 的意思都會想錯 XD。然後上面引的 axiom of infinity 裡面就有提只用到 set-theoretic axioms 的自然數建構法了 XD。