"What is a logic, and what is a proof?" (Lutz Strassburger)

キマイラ飼育記さんで紹介されていて（いつも読ませて頂いております）、日曜から読み始めた論文。こちらからダウンロード可能。
10ページ程度のよくまとまったサーベイ論文。前半の内容（論理はpreoderと見なせる）はキマイラ飼育記さんが詳しく紹介されているので、そちらを参考にしてください。後半は証明の同一性について。証明の同一性を与えるためにはpreorderではだめで、拡張して論理をcategoryと見なす必要がある。線型論理の場合proof net全体がcategoryを形成するのはよく知られており「線型論理のproofの同一性=proof netの同一性」というところまで落とせる。論文の最後で、古典論理における証明の同一性に関する最近の結果を紹介しており、それが便利です。

ここからはおそらく誰もが知っている話だろうと思うけれど、一応備忘として個人的メモ。Categoryとして論理を見る際、証明を射(arrow)と見なす。これまでの常識では、数学的objectを構成する順番は
論理式→複数の論理式の間をつなぐ二次的存在としての証明
だったが、category的見方では
証明（arrow）→arrowの特殊例としての命題*1
と、証明が第一の存在者であって命題はその特殊なケースである、と見なすこともできる。

*1:論理式Aは、identity proof id_A:A→Aで同一視できる(p6)