圏の指数の書き方は、含意記号「⊃」を使うことにします。
デカルト閉圏は、型付きラムダ計算や連言含意論理のモデルなので、いくらでも例を作れます。非自明で最も簡単な例は、二値の真偽値を圏とみなしたモノでしょう。この例はやたらに簡単なので、手作業で細部まで確認できます。つうか、細部がこれといってありません。「この世で一番簡単なデカルト閉圏」を具体的に定義してみましょう。
これから定義する圏をBとします。
- |B| = {0, 1}
- B(0, 0) = {id0}
- B(1, 0) = {}
- B(0, 1) = {t}
- B(1, 1) = {id1}
恒等射と結合の定義は明らかです。0が始対象、1は終対象となっています。
対象の直積を次のように定義します。
- 0×0 = 0
- 1×0 = 0
- 0×1 = 0
- 1×1 = 1
この定義が、実際に圏論的な直積を与えることは、しらみ潰しで確認できます。「しらみ潰し」とは言ってもとにかく数が少ないので簡単です。直積に伴う射影やデカルトペアリングも全部具体的に列挙して書き下せます。これで、B = (B, ×, 1)がデカルト圏になることがわかりました。
対象の指数を次のように定義します。
- 0⊃0 = 1
- 1⊃0 = 0
- 0⊃1 = 1
- 1⊃1 = 1
随伴性は B(x×y, z) = B(x, y⊃z) が成立すればいいのですが、これも全部列挙できて：
- B(0×0, z) = B(0, 0⊃z)
- B(0×1, z) = B(0, 1⊃z)
- B(1×0, z) = B(1, 0⊃z)
- B(1×1, z) = B(1, 1⊃z)
zも具体化すると、8つの場合になります。全部具体的に確認できます。あるいは、次の事実を使ってもいいでしょう； 普通の大小関係を「≦」と書くとして、B(x×y, z) = B(x, y⊃z) は次の命題と同じです。
- (x×y ≦ z) ⇔ (x ≦ y⊃z)
この事実の元になっていることは次のとおり：
- (B(x, y) が空でない) ⇔ x ≦ y
- (x⊃y = 1) ⇔ (x ≦ y)
随伴性の主張 B(x×y, z) = B(x, y⊃z) が二値命題論理の演繹定理を与えています。同様に、圏論的ラムダ計算の用語ではカリー化と反カリー化によるホムセットの1：1対応ですね。
演繹定理は、次の形の推論規則に出来ます。
x⊃y x
---------
y
そう、モダスポネンスです。xとyを0または1に具体化した推論図を全部列挙してみます。
0⊃0 0
---------
0
1⊃0 1
---------
0
0⊃1 0
---------
1
1⊃1 1
---------
1
モダスポネンスは、デカルト閉圏の評価射、ラムダ計算で言えば適用です。指数を計算した値の形で書くと、評価／適用の具体的な記述になります。
1 0
---------
0
0 1
---------
0
1 0
---------
1
1 1
---------
1
評価／適用を二項演算子「・」として、その演算を列挙してみるとちょっと奇妙なことになります。
- 1・0 = 0
- 0・1 = 0
- 1・0 = 1
- 1・1 = 1
1・0 の値が2種類あります。関数としての1に値0を渡して評価した値が確定しません。また、関数としての0に値0を渡した結果が抜けています。なんでこんなことになるのでしょうか？ デカルト閉圏の定義をよく確認すれば謎は解けますよ。安直な比喩に頼ると勘違いしがちです（僕も勘違いしました）。
