"Combinators and classes" (Dana Scott) - あいまいな本日の私 blog

Lecture Notes in Computer Science Vol. 37(1975) pp.1-26. こちらから入手可能。
λ計算は、Y-combinatorなどのせいで、古典論理上で単純に形式化しようとすると矛盾を導くことが知られている。また、λ項は包括原理と性質が似ている。この論文では、包括原理を持つ三値論理の集合論のモデルをλ計算のモデルを使用して構成した。

この論文では、λ計算のモデルの中で新しく言語（これが対象言語となる集合論の言語）を定義した。例えば、この言語はmembership relation $\in$ を持つが、 $a\in b$ は b(a) とλ項のβ変換で定義される。このように、対象言語の論理式＝λ計算のモデルの元となる。そして、λ抽象を（モデル内で定義された言語で書かれた）論理式に関する包括原理と見なすことにより、包括原理を持つ素朴集合論がモデルの中で展開可能である。しかし、残念ながら（というか予想通りと言うか）等号はintentionalなため、外延性を持たない。
さて、λ計算のモデルを扱うメタ理論として超限帰納法が可能な理論をとろう。こうすると、超限帰納法により対象言語の真理述語 ${\cal T}$ と ${\cal F}$ が定義可能である。かくして、当初のモデルを拡張し、包括原理を持つ集合論の真理定義（モデル）を得ることが出来る。もちろん ${\cal T} a$ は $a$ と同値である。
一方、対象言語では

真理定義 $\lambda x. x$ が可能であり（ $\varphi\leftrightarrow(\lambda x. x)_{\varphi}$ ）、
ラッセル集合 $\lambda x. x\not\in x$ も定義可能である

ために、 ${\cal T}$ と ${\cal F}$ の両方に含まれない論理式が存在する（ $(\lambda x. x\not\in x)\not\in {\cal T}, {\cal F}$ ]）。すなわち、この体系はパラドックスを回避するために三値論理になっている。

超限帰納法で構成されているだけに、この集合論は記述力に関してかなり強力である。Martin-Lofの直観主義的タイプ理論と同じく、universeの階層を持つ。
この論文は、Aczelのフレーゲ構造などでも引用されており、combinator によって包括原理と論理を解釈するというアイディアは一般性を持つものなのだろう。
（後で内容を追加します）