今読んでいることになっている論文たち

本日、資料整理をしたところ、机の上にプリントアウトの山を発見しました。どれも途中まで読みかけで、そして紛失したと思っていたものばかり。自分でもタイトルを忘れていたので、備忘を兼ねてメモっておきます。

"Cut elimination for Zermelo's set theory" (Gilles Dowek and Alexandre Miquel)

Tさんから紹介された論文、こちらにpdfファイルがあります。この論文はなくした後、もう一回プリントアウトして読むもまた紛失し、再度プリントしました。今回は、最初にプリントアウトした版が出て来ました。この論文は一応読んではいます。
証明論における無矛盾性証明といえば、典型的なのが cut eliminationです。しかし、通常、cut eliminationは公理系には適用できません。この論文では、まずある型理論（というか項書き換え系）を定義し、その型理論がZの保存拡大になっていることを示しています。その際には、Aczelのやり方を応用し、集合を有向グラフとして翻訳しました。そして、その理論の正規化定理を証明しました。すなわち、結果的にZと同値な型理論のcut eliminationを成し遂げたことになります。快（怪）作です。スゴいので、ぜひ読んでください。
集合論を型理論に変換して正規性を証明することの何が難しいかというと、Zでは正規化不可能な証明を持つ定理が存在するということです。例えば、任意の集合 $a\in V$ に関して、集合 $b=\{ x: x\in a \,\& \, x\not\in x\}$ を考えます。b はもちろん Axiom of Separation から構成可能です。しかし、 $b\in b$ という文を考えると、この文は $b\in a \, \& \, b\not\in b$ に書き換えられ、そしてこれは $b\in b$ へと再度書き換え可能です。つまり、この書き換え系は無限ループしてしまうことになります（Russell paradoxの一般化！）。もちろん、Zでは $b\not\in a$ が以上の議論から結論され、パラドキシカルなことは何もありません。問題は、この定理 $b\not\in a$ の証明は、（おおざっぱに言うと）「 $b\in a$ を仮定すると無限ループする」というもののため、この証明は正規化不可能であることです（正確にはCrabbeを参照のこと）。
Aczelのやり方は、集合を有向グラフとして考え、集合間の同一性を二つのグラフの間のbisimulationが存在することによって定義します。 $a\sim b$ でグラフ aとbの間にbisimulationが存在することを表しましょう。このとき、 $x\in b$ は、Zでは上で見たように $x\in a \,\&\, x\not\in x$ に書き換えられましたが、Aczelのやり方では $(\exists y)y\sim x \,\&\,(y\in a \,\&\,y\not\in y)$ に書き換えられます。つまり、 $b\in b$ は
　　 $(\exists y)y\sim b \,\&\,(y\in a \,\&\,y\not\in y)$
を意味します。このとき、 $b\in b$ ではなく、 $y\not\in y$ （yは変数）が得られます。そして $y\not\in y$ を無限ループさせることは出来ません。このように、直接 b を代入するのではなく、b とは異なる別のグラフ y （ただし $y\sim b$ を満たす）を途中に一個かませることで、無限ループへ陥ることを防ぐ訳です。巧妙だ。

"Sets in Types, Types in Sets" (Benjamin Werner)

これもTさんから紹介された論文。途中まで読むも、2ヶ月で紛失、やっと見つけた。こちらからダウンロード可能。
CoquandらのCalculus of Construction にinductive data type を加えることで拡張した Calculus of Inductive Construction (CIC) を考える。本質的には

依存型理論（Curry-Howard 対応によって命題を型として表現）
以前のエントリで紹介したように、impredicative なlevelを持つ
Martin-Lofの直観主義的型理論と同じく、predicativeなUniverseの階層を持つ（ $\langle Type_i :i\in\omega\rangle$ ）
Godelの System T における primitive integers を一般化した、inductive type を持つ

証明支援系のCoq.やLegoは、多少の相違はあっても、CICを実装したものと見なすことも出来る。この論文は、CIC+TTDA+排中律に公理的集合論 ZFC を埋め込む、という話。ちなみに、公理TTDAは与えられたモデルがfullであることを保証するものである（詳細は略）。
ZFCで定義された集合をCICに埋め込む際には、AczelがAFAの定式化の際に使用して有名になった集合を有向グラフと見なす（集合を点、membership関係をarrowと見なす）やりかたを型理論的に抽象化して採用。公理に関して、埋め込みの際に問題となるのはreplacementとchoiceの処理。最終的には、 $V_{\kappa_i}$ （ただし $\kappa_i$ はi番目のinaccessible cardinal）を $Type_{i+2}$ に埋め込むことが可能となった。ついでに、著者は実際にCoq.でZFCの翻訳を実装した。

"Stratification and Cut elimination" (Marcel Crabbe)

JSL vol.56 pp213-226 (1991).
Quineの NF から外延性公理を除去した部分体系 SF について cut elimination（というか実際には normalization）を行う。Miquelらの論文で参照していたので読み始める。はじめの方の説明は有益、しかし具体的なSFのモデル構成のところでめげ、その後論文の紙が行方不明に。