今読んでいることになっている論文たち - あいまいな本日の私 blog本日、資料整理をしたところ、机の上にプリントアウトの山を発見しました。どれも途中まで読みかけで、そして紛失したと思っていたものばかり。自分でもタイトルを忘れていたので、備忘を兼ねてメモっておきます。 "Cut elimination for Zermelo's set theory" (Gilles Dowek and Alexandre Miquel) Tさんから紹介された論文、こちらにpdfファイルがあります。この論文はなくした後、もう一回プリントアウトして読むもまた紛失し、再度プリントしました。今回は、最初にプリントアウトした版が出て来ました。この論文は一応読んではいます。 証明論における無矛盾性証明といえば、典型的なのが cut eliminationです。しかし、通常、cut eliminationは公理系には適用できません。この論文では、まずある型理論（というか項書き換え系）を
