ワーイ、完結だ。シリーズがちゃんと完結するなんて、滅多にないよ、僕は。
前回の最後（一部省略・短縮）：
論理の定義として閉包作用素を使う定義があります。これについて説明するかも知れません。ストラスバーガーの意図としては、論理をプレ順序と考えるのは中間ステップであり、論理を圏として捉えるのが目的なので、「論理は圏だよ」という結論にたどり着かないと心残りかも知れません。
閉包作用素による論理の定義は、単品メニューとして出せる話題なので今回は省略して、「論理は圏だよ」という話をして、ストラスバーガー論文の紹介を締めくくりたいと思います。
内容：
今までの復習
まず、次の大きな前提を置きました。
- どんな論理（論理的システム）でも、命題（正確には論理文）の集合Sを確定できるだろう。
- どんな論理でも、「ならば」の概念があり、それは命題の集合Sの上の二項関係とみなせるだろう。
さらに、「ならば」に関して次を仮定しました。
- 命題A（A∈S）が何であっても、「AならばA」。
- 命題A, B, C（A, B, C∈S）に対して、「AならばB」と「BならばC」が言えるなら、「AならばC」。
「ならば」を「≦」と書き換えてみると：
- A∈Sに対して、A≦A 。（反射律）
- A, B, C∈Sに対して、A≦B かつ B≦C ならば A≦C 。（推移律）
これで、(S, ≦)はプレ順序集合になりますから、「論理とはプレ順序集合だ」と主張できるわけです。主張という言葉が強すぎるなら、「論理をプレ順序集合と見なそうじゃないの」という提案だと言ってもいいです。ストラスバーガーは*1そんな提案をしています。
状況証拠を確認
「論理とはプレ順序集合だ」は、ほんとに妥当な提案でしょうか。なんらかの論理があるときに、それをプレ順序集合(S, ≦)と見なせるかを検証する必要があります。まず、伝統的な「構文論（証明論）／意味論（モデル論）」という分類*2にしたがって考えることにして、A, B∈Sに対して：
- 証明論的システムにおける A≦B とは、A |- B （Aを仮定してBを証明できること）。
- モデル論的システムにおける A≦B とは、A |⇒ B （Aを満たすモデルは常にBも満たすこと）。
とすれば、(S, ≦) がプレ順序集合になります。左側が空っぽの |- A とか、左側が複数の文からなる A, B |- C とかも、次のように処理できます。
- |- A を T |- A と考えて、T≦A 。
- A, B |- C を A∧B |- C と考えて、(A∧B)≦C 。
あるいは、文の有限集合を改めて文と考えれば：
- |- A を {} |- {A} と考えて、{}≦{A} 。
- A, B |- C を {A, B} |- {C} と考えて、{A, B}≦{C} 。
また、別なケースとして、文の集合Sの部分集合Kが指定されていて、Kに属する文は真だと思える（Kがセオリーである）ときは：
- A≦B ⇔ ‘A⊃B’∈K
としてプレ順序集合(S, ≦)が定義できます。
これらの事実は、「論理とはプレ順序集合だ」を認めてもいい状況証拠を与えるのですが、それと同時に、論理記号T（真）、∧（連言）、⊃（含意）や文の有限集合の使い方や意義を印象的に示しています。
プレ順序集合から圏へ
プレ順序集合(S, ≦)は、特殊な圏とみなせます。（「はじめての圏論 その第3歩：極端な圏達」を参照。）
- 対象の集合はS（Sは文の集合）。
- a≦bのとき、a→b という射が1つだけ存在すると考える。
- その他の射はない。
ホムセットが空（empty）か単元（singleton）である圏をやせた圏と呼ぶので、「プレ順序集合＝やせた圏」です。
しかし、論理を表現する圏が必ずしもやせている必要はありません。むしろ、ふとって(?)いたほうが好都合なのです。というのも、論理を表す圏における射を「命題から命題を導く証明」と解釈したいからです。
「証明が射」 -- ピンとこないかも知れませんから例を出しましょう。第2回で一次方程式の証明系を出したので、これで考えましょう。次は連立一次方程式を解く過程です。「解く過程」とは、実は証明です。
- {2y - 8 = 0, 2x + 3y = 0}
- {2y = 8, 2x + 3y = 0}
- {y = 4, 2x + 3y = 0}
- {y = 4, 2x + 12 = 0}
- {y = 4, 2x = -12}
- {y = 4, x = -6}
箇条書きの各段階における連立方程式（一次方程式の集合）をE1, E2, ... のように表すとすると、これは、E1→E2→E3→E4→E5→E6 と書けます。ここで矢印は、基本的な等式変形を意味します。合理的な等式の変形（基本的でも複雑でも）を矢印で表し、必要に応じて名前を付けると、次が成立します。
- Eが連立方程式として、「何もしない」等式変形 E→E がある。
- E, F, Gが連立方程式として、f:E→F、g:F→G が等式変形なら、“fの次にgを行った等式変形”も合理的な等式変形である。
無数の連立方程式達のあいだに、等式変形という無数の矢印が張り巡らされた状況ですね。これって、… そう圏ですよね。実際に圏であることを確認するのは練習問題。
太った圏も認めよう
2つの命題A、Bがあるとき、「Aを仮定してBを結論する証明が（あっても）ただ1つだけ」というのは不自然です。実際には、複数の証明があることが多いでしょう。ある論理的システムLにおいて、AからBを導く証明の全体をProofL(A, B)としましょう。AとBが色々変われば、証明の集合ProofL(A, B)が空集合になる時もあるでしょうし、ProofL(A, B)がもの凄くデカイ集合になるかもしれません。つまり、1つ1つの証明を区別して取り上げれば、論理から作られる圏は太っているのです！
となると、「論理はプレ順序だ」＝「論理はやせた圏だ」は一般性に欠けるわけで、「論理は（やせているとは限らない）圏だ」となります。やせてなきゃダメという制限は外すべきなんです。誤解されると困るから言っておくけど、「太っていてもいい」は、「やせていてはダメ」を意味しませんよ、「やせていてもいいし、太っていてもいい」ってこと（何の話をしてるか分かんなくなるな）。
圏としての論理
さて、「論理は圏だ」と定式化すると、なにかいいことがあるでしょうか？ 当たり前のことですが、圏論の概念や技法を論理に持ち込めます。例えば、圏論の基本概念である関手や自然変換を論理に対して使っていいことになります。
第1回で、ナントカ論理／カントカ論理がウンザリするほどあると言いましたが、それらの論理達が無関係というわけではありません。例えば、命題論理は述語論理の一部として埋め込めます。∨、∧、¬を使う論理と、⊃と⊥を使う論理は相互翻訳可能です。直観主義論理の証明は古典論理の証明とみなせます。こういった相互関係は、圏（として定式化した論理）のあいだの関手として表現可能です。
2つの論理が事実上同じことはよくあるのですが、この事態は、“2つの圏が同値である”という形でうまいこと表現できます。圏の同値性には自然変換が必要なので、系統的な命題の書き換えとしての自然変換も“自然に”出現します。
「証明とは何か？」とは何か？
最後に、ストラスバーガーの問題意識を（僕が理解できる範囲で）少しだけ説明しましょう。
論理と圏の対応関係がうまくいっている例として直観主義論理があります。命題を圏の対象、証明を圏の射と考えて次のような対応があります。
- 真 T ←→ 終対象 1
- 連言 A∧B ←→ 直積 A×B
- 含意 A⊃B ←→ 指数ベキ BA
- モダス・ポネンス*3 A, A⊃B |- B ←→ 評価射 ev: A×BA→B
- 演繹定理 ←→ A×(-)（(-)×Aでも事実上同じ）と(-)Aの随伴性
終対象、直積、指数ベキなどがうまく定義できる圏は、デカルト閉圏（Cartesian closed category; しばしばCCCと略記）という圏です。よって、“直観主義論理←→デカルト閉圏”の対応があるわけです。 ただし、直観主義論理の証明を正規化したものを射と考えないとキレイな対応はとれません。
（僕はよく分かってないが）線形論理とスター自立圏（*-autonomous category）のあいだにもキレイな関係があるそうです。ここでも、証明を、標準的な形にして整理しないとうまい対応は作れません。余談ですが、デカルト閉圏もスター自立圏もラムダ計算のモデルに使われています -- ようするに、論理計算も関数計算も同じようなもの（カリー・ハワード対応）ってことですね。
さてそれでは、我々にとって一番お馴染みで一番基本的な古典論理はどんな圏と対応しているのでしょうか？ ストラスバーガーによれば、なんと、古典論理（ブール論理）に対応する圏が一筋縄では定義できないそうです。古典論理の証明を、標準的な形にして整理する部分が難しい、と。そこで、"What is a proof?"なる問＜とい＞がシリアスになるわけです。… が、これ以上は僕の手に余るので、原論文や関連文献をあたってみてください。
お後がよろしいようで。
