tips: 包括原理でλ項を表現する

C大学のKm先生より一昨年に教えて頂いた話を今日再確認する。"Logic Without Contraction as Based on Inclusion and Unrestricted Abstraction" (Uwe Petersen), Studia Logica. 64.365-403 (2000). この話はp381-382に書いてある。

包括原理を持つ集合論では全てのλ項を表現することができる、というある意味驚きだがある意味当たり前な話。
普通の表記に書き直すと、大まかな話では

1. λ項 λx.fx は集合 {: y=fx} と書き直す
2. λ項 s,t の適用(juxtaposition) st は {x :(∀y)[∈s → x∈y]} と書き直す
3. β-変換 (λx.Px)t = P[t] は包括原理 t∈ {x:Px} ⇔P[t] そのもの

だそうです。包括原理のある集合論では外延性公理が仮定できないので、pair の定義には工夫が必要です。
{x:Px}も特殊なタイプのλ項だと見なすことができるので、その意味でPetersenは両者の同値性を証明した、と見なしてもいいのかもしれない。

ちなみにPetersenは普通 {x:P(x)} と書く集合のことを λx.Px と書いている(Schutteの影響？）ので、一般的なλ項を表現するために "in somewhat adapted notion of lambda calculus λx.θ[x]"(p381)と書いたりして、えらくややこしい。