たまたま、"What is a logic, and what is a proof?" (April 8, 2005) by Lutz Strassburgerという論文を見つけて、読んでみました。比較的短い（印刷して12P）解説的な論文です。表題のとおり、
- 論理とはなにか？
- 証明とはなにか？
という2つのテーマを扱ってます。後半1/3程をしめる「証明とはなにか？」が僕はよくわからんかったのだけど、前半は、「論理（a logic）は圏だよ」という主張をとても上手に説明しています。で、まー、この前半部分を紹介しようかと。
ただし、以前に書いたエントリーを参照しながら私見を交える（私見のほうが多いかな）ので、上記論文の忠実な紹介にはなってません。気になる方は原文を読んでくださいね。
今回の内容：
プレ順序集合
集合Xと、X上の二項関係‘≦’が次を満たしているとき、(X, ≦）をプレ順序集合（preordered set）と呼びます。
- x∈Xに対して、x≦x 。（反射律）
- x, y, z∈Xに対して、x≦y かつ y≦z ならば x≦z 。（推移律）
普通の順序集合は、これに加えて反対称律「x≦y かつ y≦x ならば x = y」も満たします。プレ順序集合は反対称律を要求しません。当然ながら、順序集合は常にプレ順序集合です。
「はじめての圏論 その第3歩：極端な圏達」で述べたように、プレ順序集合はやせた圏（thin category）と同じものです。図形的に考えたいなら、頂点xごとに自己辺（ループ）selfxが指定されている有向グラフを考えます。こういう有向グラフは反射的有向グラフ（reflexive directed graph）と呼ばれます（「有向グラフの指数（exponentiation）」 に出てきました）。反射的有向グラフがあるとき、頂点xとyのあいだに：
- xからyに至る有向経路（有向辺の列）があるときに x≦y
と定義します。すると、頂点の集合はプレ順序集合（そして、やせた圏）になります。
論理とはプレ順序集合なり
質問"What is a logic?" に対するストラスバーガー（Strassburger）の答えは、実にアッサリしていて、「それはプレ順序集合だ」となります。
なんでこんな答えになるのか、というと、「ならば」の概念がキーとなります。命題AとBのあいだに、「AならばB」という関係があるとき、不等号を使って「A≦B」と書くことにします。「A≦B」より「A≧B」のほうがいいだろう、とかの“向き”の議論は毎回僕を悩ますものですが、ともかく今回は「≦」にします！
どんな論理であっても、次の2つのことを基本にしている、と考えていいでしょう。
- Aが何であっても、「AならばA」。
- 「AならばB」と「BならばC」が言えるなら、「AならばC」。
これはつまり、命題の集合をSとすると：
- A∈Sに対して、A≦A 。（反射律）
- A, B, C∈Sに対して、A≦B かつ B≦C ならば A≦C 。（推移律）
よって、(S, ≦)はプレ順序集合というわけです。
文と帰結関係
もう少し正確な話をしましょう。まず、命題という用語はやや曖昧なので、論理文（logical statement/sentence）、あるいは単に文と言うことにします。
どんな論理（論理的なシステム）であっても、“論理文の集合S”を持つと考えてよさそうです。例えば、命題論理（言明計算）なら、命題論理式が文だし、述語論理なら自由変数を持たない論理式を文と考えるのが普通です。自由変数を許した論理式を文と定義することもできそうです。詳細はともかくとして、論理ごとに論理文の集合Sが（そうしようと思えば）確定できることは、あまり異論がないかと思います。
ところが、「ならば」に関してはいろいろなレベルの、いろいろな意味を持つ「ならば」が存在します。このことは「さまざまな『ならば』達」で述べました。とりあえず、問題にしている論理が証明論的システムならば証明可能性（以前使った記号は「|-」）、モデル論的システムならば伴意関係（以前使った記号は「|⇒」）を「ならば」として採用しましょう。混乱を避けるために、「ならば」を表す関係≦を帰結関係（consequence relation）と呼びます。
まとめると、A, B∈Sに対して、
- 証明論的システムにおける帰結関係 A≦B とは、Aを仮定してBを証明できること
- モデル論的システムにおける帰結関係 A≦B とは、Aを満たすモデルは常にBも満たすこと
個別の論理達から論理の一般論へ
説明の便宜上、証明論的システムとモデル論的システムに分けました。しかし、ストラスバーガーの意図は、そういう区別や流儀を越えて、より一般的な“論理の定義”を提出することです。
実際、ナントカ論理／カントカ論理という区別や流儀にはウンザリ。ほとんど常に、命題論理と述語論理は区別されますが、この区別は教育的に有害じゃないかと僕は思っています。構文論（証明論）と意味論（モデル論）の区別もまた伝統的です -- これは区別したほうがいいかも知れない、、、たぶん。
論理式にどんな論理記号を許すかも、すごくバリエーションがあります。∧、∨、¬が一番普通でしょうが、⊃（含意）と⊥（矛盾）を採用する流儀もあります。論理記号を1つだけしか使わない体系もできます（これ変態ですけど）。許される推論の多寡＜たか＞によって古典論理と直観主義的論理、その他のナンタラ論理に別れるし、様相記号や、さらにもっと目新しい論理記号を入れた体系もあります。（形式的）証明もヒルベルト方式、ゲンツェン方式（シーケント計算）、タブロー方式なんてのがありますね。
こういう多様性は「論理の豊饒＜ほうじょう＞さ」を示すものでしょうが、僕は、「なんだか博物学・分類学みたいだなー」とも感じます。ストラスバーガーの質問と答えは、こういう不満感を多少は解消してくれます。
続くのかな
実は1回読み切りで書き切ろうと思っていたのですが、疲れちゃったよ。
とりあえず、「論理（論理的システム）はプレ順序集合だ」とは言いましたが、既存のさまざまな論理的システムが、ほんとにプレ順序として定式化できるのか？ が問題になります。そして、「プレ順序集合＝やせた圏」という事実を発展させて、論理的システムそれ自身を圏と考えること、さらには、論理的システム全体からなる圏が考えられないか、とかが次の話題となりますね。
