哲学者のための圏論入門 ∗森田真生（独立研究者）

1 はじめに1945 年、Samuel Eilenberg と Saunders Mac Lane による論文 General Theory of
Natural Equivalences が発表され、圏（category）という言葉が、はじめて数学の表舞台に登場しました。もともとこの論文は、そのタイトルにもある通り、代数的位相幾何学（algebraic topology）の文脈で、当時ますます重要な役割を果たしつつあった自然変換（natural transformation）の概念の一般理論を構築することを目的に書かれたものでした。自然変換の概念を厳密に定式化するために、その背景にある関手（functor）の概念が導入され、さらに関手を定義するために、圏の概念が要請されたわけです。この時点で圏の概念は、あくまで自然変換の概念を支えるための二次的なものと見做されていました。実際、1945 年の論文の中には It
should be observed first that the whole concept of a category is essentially an auxiliary
one; our basic concepts are essentially those of a functor and of a natural transformation(...). とあって、圏の概念が、自然変換と関手の理論を構築するための補助的なものにすぎないことが、あらためて強調されています。[7] によれば、Eilenberg は「これが純粋圏論（pure category theory）を扱った最初で最後の論文になるだろう」と信じていたそうですから、「圏論」がそれ自体数学の対象として真面目に研究されるようになること、ましてや「哲学者のための圏論入門」などというセミナーが開催され、そこに非数学者が何人も集って勉強をするような日が来るなどとは、夢にも思わなかったに違いありません。
冗談はさておき、Eilenberg らの当初の予見とは裏腹に、はじめこそ補助的な道具として背景に控えていた圏の概念も、みるみるうちに存在感を持つようになっていきます。圏の言葉は、1940 年代の当初から、代数的位相幾何学の諸概念を整∗本稿は応用哲学会サマースクール 2013「哲学者のための圏論入門」の参加者に向けて作成された講義用配布資料です。講義は板書中心に進めるため、当初は１-２ページの簡単な講義概要だ
け作成しようと考えていたのが、勢い余って 40 ページを超えてしまいました。本稿はあくまで講義をサポートするための補助資料として作成されたもので、いかなる意味でも self-contained なテ
キストを目指して書かれたものではないことをあらかじめご了承ください。（最終更新日: 2013 年
9 月 16 日）

1理するための道具として大きな力を発揮しました。そうした中で、はじめは自然変換の背景にあった関手の概念の重要性が、次第に認識されるようになっていきます。1950 年代に入ると、グロタンディークらにより、関手がなす種々の圏（functor
categories）を使って、代数的位相幾何学や代数幾何学の分野で新しい強力な手法が次々と開発されます。1960 年代には、F. W. Lawvere の仕事を中心として、圏と論理の間の驚くべき関係性が次々と明らかになり、圏論による論理学（categorical
logic）の時代が幕を開けました。さらに 1970 年代に入ると、計算機科学のみならず、言語学や認知科学、哲学など、純粋数学の外でも、圏論的な方法や言語の導入が試みられるようになっていきます。
いまでは控えめに言っても、圏論が現代数学の欠くべからざる道具であることは、多くの数学者が認めるところになっていると思います。しばしば、「圏論は既知の概念を整理するための便利な道具だ」という言い方をされることがあります
が、代数幾何学や論理学における縦横無尽の圏論の活躍を目にすれば、それが単なる整理のための道具でなく、数学的思考と想像力の新たな通路を開く、真に創造的な道具であるということを、納得できるのではないかと思います。この４日間の講義で、そんな圏論の可能性と創造性の一端だけでも、みなさんと共有することができたらと思っています。

function の一般理論

2ζ という字を見ただけで、思わず頬が弛んでしまうのを「ゼータ笑い」というそうです。私は残念ながらゼータ笑いをするほどの数論の素養がないのですが、同じ記号を前にして、そこから想起されるものが実に人それぞれなのは、興味深いことです。そういえば、「 p が素数であることを示せ」という問題に対して「 p だから素数です」と答えるジョークを聞いたことがありますが、数学をやっていたら、やっぱり p なら素数に、n なら自然数に見えてしまいます。 p = 4 とか、n = 1.15
とか書かれると、なんとも落ち着きません。
それはさておき、同じ記号列に対して、数学者によってそれぞれ想起するものが違う、ということも多々あります。たとえば A → B という記号列は、ある人には位相空間の間の連続写像に見えて、またある人には環の準同型に見えるかもしれません。またある人にはプログラムの型に見えて、またある人には関手の間の自然変換に見えるかもしれません。1 まぁ、実際には、同じ人の頭の中でも、こういういろいろな視点を柔軟に行ったり来たりしながら数学をするわけですが、普通、同じ論文の中で同じ記号の意味がコロコロ変わるということはありません。トポ
それにしても、ひとたび A と B が関手だと思って眺めていると、いかにも A → B が自然変換に見えてきて、自然変換の component まで見えてきそうになるし、やっぱり環の準同型だと思って眺めると、単位元が移る様子まで見えてきそうになるから、不思議なものです...。
12

ロジーの論文を読んでいるときに、「おや？A → Bって、もしかしてプログラムの型のことかな？」なんて思う人はいないでしょうし、逆に証明論の本を読んでいるときに「ん？もしかして A → Bって、C ∗ 環 の間の準同型のこと？」と心配にな
ることもないでしょう（たぶん）。
ところが、これから学んでいく圏論はいわば、あらゆる具体的な文脈から解放された「矢印」たちそのものについての一般理論です。数学に現れる具体的な A → B
たちの振る舞いに共通する普遍的な性質を抽象することによって、圏論における「矢印（arrow）」の概念が得られます。そして圏論の世界では、この矢印たちが主役になるのです。
さて、それではいったい「具体的な A → B たちの振る舞いに共通する普遍的な性質」とは、何でしょうか。ここでさしあたり、数学の中に登場する様々な A → B
たちを総称して、function と呼んでみることにしましょう。素朴に考えて、A → Bと書かれていたら、A から B への何かしらの対応関係があるように見えます。このような対応関係を表す言葉として、しばしば数学では function という言葉が使われます。私たちがいま考えたいのは、このような function たち一般についての理論です。ところが、この function という概念がまた、一筋縄には行きません。functionとは、いったい何でしょうか？
集合論的に見ると、function は、それ自体もひとつの集合に過ぎません。具体的には、集合 A, B に対して、二項関係 f ⊂ A × B であって、A の任意の元 a に対して、(a, b) ∈ B となる B の元 b がただひとつ存在するようなもののことを A から B へのfunction と呼んで、それを f : A → B と書きます。つまり、function をそのグラフと同一視してしまうわけです。これはこれで、数学的には首尾の一貫した見方ではありますが、 f : A → B を A × B の部分集合と見做すという視点からは、functionの概念が本来内包している、操作的な側面やダイナミックな側面が捨象されてしまっています。いわば、徹底して静的（static）な function 観であると言うことができるでしょう。
実際に数学者が function を運用する際には、もう少し素朴な見方をします。たとえば、集合 A と B の間の写像 f : A → B は、「集合 A の各元 a に対して、集合
B の元 f (a) を対応させる規則」として定義されます。ここには、集合 A の「中身」
を集合 B の「中身」に移す 2 のが function である、という見方があります。これならば、先ほどの場合とは違って、function の操作的な側面がはっきりと見えてきます。しかし、ある対象の「中身」を別の対象の「中身」に移すのが function である、という function 観は、これはこれで限界があります。なぜならば、一般に function
A → B があったときに、そもそも A や B に「中身」があるとは限らないからです。
2

この「移す」が「映す」や「写す」に見えてくると、少しずつ圏論に近づいていきます。

3たとえば、A → B を、命題 A からの命題 B の導出と見たときに、命題 A の「中身」とは何でしょうか？あるいは、A → B を関手 A から関手 B への自然変換と見たときに、関手 A の「中身」とは何でしょうか？少なくともこうした場合には、集合のときのように、素朴に「対象の内部に立ち入る」ということは、できそうもありません。
ある対象を、その「内部に立ち入って」見る視点のことを internal な視点と呼ぶ
ことにしましょう。すると、集合論的な数学観は、本質的に internal なものになります。そもそも集合論は、集合と所属関係「∈」3 だけから成り立っているわけですから、すでにある集合から新しい集合をつくるか、あるいは所属関係によってある集合の中身に立ち入るか、しかありません。先ほど集合論的に写像 f : A → B
を定義するときに、A と B から新しい集合 A × B をつくり、その「中身」として fを定義したのなどは、その好例です。そういう意味で、function をそのグラフと見做す視点は、徹底的に internal な視点ですし、その後に見た素朴な写像の定義もまた、集合の中身に立ち入る必要があるという意味で、やはり internal な見方であると言えるでしょう。
しかし、先ほど挙げた例のように、A が命題であったり、A が関手であったりする場合には、その「中身」に立ち入るというのがどういうことかが、いまひとつ
はっきりしません。そこで、こうした場合も含むより一般的な function の理論をつくるためには、internal な視点を排除して、external な視点、すなわち、対象の内部に一切立ち入らない視点で進んでいく必要がありそうです。それでは、external な視点から見た function は、いったいどのような性質を持っているものでしょうか？

2.1

写像再考

ここではまず、internal な視点によって定義された集合とその間の写像を、あらためて external な視点から見たときに見えてくる性質を、いくつかリストアップしてみることにしましょう。

• 始域（domain）と終域（codomain）の存在
まず、写像には、必ず始域（domain）と終域（codomain）があります。当たり前ですが、写像というのは必ず「どこか（始域）から、どこか（終域）への写像」なわけです。始域が A で、終域が B であるような写像を f : A → Bと書きます。写像には始域と終域がある、というのは、写像の持つ externalに記述できる性質のひとつです。

そう思ってみてみると、∈ というのが、集合の中身を覗き込もうと、右に向けてパッと照らされたスポットライトのようにも見えてきます。いや、見えないか...。
34

• f : A → B と g : B → C に対する、合成 g ◦ f : A → C の存在
２つの写像 f : A → B と g : B → C があると、その合成 g ◦ f : A → C を、
(g ◦ f )(a) := g( f (a)) によって定義することができます。この定義そのものはinternal になされますが、それを external な視点から見れば、「写像 f の終域と g の始域が一致してたら、その合成 g ◦ f も存在する」と言っているわけですから、これもまた、写像の持つ external な性質です。
• idA : A → A の存在
どんな集合 A に対しても、idA (a) = a によって、恒等写像を定義することができます。どんな A に対しても A から A 自身への写像が必ず１つは存在するというのは、ひとたびその写像の internal な定義を忘れてしまえば、やはり
external な性質として書くことができます。
• f : A → B, g : B → C, h : C → D に対し、h ◦ (g ◦ f ) = (h ◦ g) ◦ f
写像は合成に関して結合的です。実際、(h ◦ (g ◦ f ))(a) = h((g ◦ f )(a)) = h(g( f (a)))((h ◦ g) ◦ f )(a) = (h ◦ g)( f (a)) = h(g( f (a)))
が任意の a ∈ A について成り立ちます。
これも、internal な根拠は忘れて、とにかく写像の合成に関する結合性という結果だけ見れば、やはり external に記述できる写像の性質です。

• f : A → B に対し、 f ◦ idA = f = idB ◦ f
恒等写像の「何もしない」という性質は、internal には idA (a) = a という写像の定義によって与えられるわけですが、この性質は結果として、他の写像との関係性の中に external に表れます。実際、任意の写像 f : A → B に対して、( f ◦ idA )(a) = f (idA (a)) = f (a)(idB ◦ f )(a) = idB ( f (a)) = f (a)です。任意の写像 f : A → B に対して、 f ◦ idA = f = idB ◦ f が成り立つというのは、external に記述できる恒等写像の性質です。
以上、集合の間の写像を external な視点から眺めたときに見えてくる、いくつかの性質をリストップしてみました。どれもほとんど自明というか、たいしたことのない性質のようですが、こうした自明にも見える性質を、ひとつひとつ丁寧にピックアップしてくることが重要です。そして、結果的には、ここでリストアップ
した諸性質が、私たちが function と呼ぶことにしたかなり広範の A → B たちに当てはまることが分かります。このリストは、案外、function というものの本質を捉えているのかもしれないのです。
実は、このリストはほとんどそのまま圏の定義になっています。

5

2.2

圏の定義

いよいよ圏の定義を紹介します。実は前節のリストによって、圏の定義は実質的には与えられてしまっているのですが、改めてここに、圏の定義を書き下してみることにしましょう。
定義 2.1 圏（category）とは、以下のデータの集まりであって、(as) と (id) を満た
すもののことを言う：• 対象（object）A, B, C, . . .
• 射（arrow, morphism） f, g, h, . . .
• 各射 f に対して f の始域（domain）と呼ばれる対象 dom( f ) と f の終域（codomain）と呼ばれる対象 cod( f )（以下、A = dom( f ) かつ B = cod( f ) であることを、 f : A → B と表記することにする）．
• cod( f ) = dom(g) なる射 f, g に対して f と g の合成（composite）と呼ばれる射 g ◦ f : dom( f ) → cod(g)．
• 各対象 A に対して、A の恒等射（identity arrow）と呼ばれる射 1A : A → A．
(as) 任意の f : A → B, g : B → C, h : C → D に対し h ◦ (g ◦ f ) = (h ◦ g) ◦ f ．
(id) 任意の f : A → B に対し、 f ◦ 1A = f = 1B ◦ f ．
圏の定義は、以上です。
圏 C の対象全体の集まりを Ob(C) と書いたり、C0 と書いたりします。また圏C の射全体の集まりは Ar(C) と書いたり、C1 と書いたりします。また、圏 C の対
象 A, B に対して、A から B への射全体の集まりを HomC (A, B) と書きます。ここで、一般に C0 や C1 や HomC (A, B) は集合になるとは限らないことに注意してください。特に、C1 が集合になるような圏 C を小圏（small category）と呼び、また任意の A, B に対して HomC (A, B) が集合になるような圏を局所小圏（locally small
category）と呼びます。また、C0 や C1 が実際には集合でない場合にも、「C の対
象 A」という意味で A ∈ C0 と書いたり、「C の射 f 」という意味で f ∈ C1 と書いたりしますので、あらかじめご留意ください。
さて、ここまで読んできてくださってきた方には、圏の定義はいかにも「自然」に見えるのではないでしょうか。このシンプルな定義が、実に広範にわたる数学の現象をカバーします。その詳細については、講義の中で丁寧にお話をさせていただくことにいたしましょう。

6

3 講義の概要
それでは以下簡単に、４日間 12 コマの講義の概要と流れをまとめておくことにいたします。講義は基本的に板書を中心に進めていきますが、全体の流れを把握するために必要があれば、このレジュメを活用していただければと思います。

第１講． 圏の定義と例
初日の冒頭は、圏論の簡単な歴史を紹介した上で、圏を定義し、いくつかの重要な例を紹介します。

第２-３講． 普遍性による対象の定義
とことん external な視点で数学をする、というのが圏論の基本的な思想であり、醍醐味でもあります。いままでだったら安易に対象 A の内部に立ち入って（a ∈ A）
いたところを、ぐっと踏みとどまってみるのです。
対象の内部に立ち入らないで、いったいどうやって数学ができるのだろう、と疑問に思われるかもしれません。たとえば、対象として集合を考えているとしたら、対象 A の内部に立ち入らないということは、A の元をとらないということです。集合の元をとらないで、いったいどうやって数学をしようというのでしょうか？
それが、意外なほど、いろいろなことができてしまうのです。簡単な例を紹介しましょう。集合の間の写像について、単射と全射という概念があります。念のため、定義を書いておきましょう。
定義 3.1 写像 f : A → B について、(1) f が単射（injection）であるとは、A の任意の元 a, a′ に対し、
f (a) = f (a′ ) ⇒ a = a′が成り立つことを言う。

(2) f が全射（surjection）であるとは、 B の任意の元 b に対して、A の元 a が存在して、 f (a) = b となることを言う。
見ての通り、単射性や全射性は、写像が与える集合の中身の対応関係についての性質ですから、これは集合の内部に立ち入ることではじめて定式化できるもののように思えます。ところが、写像の単射性や全射性は、実は集合の中に一切立ち入ることなく、他の写像との関係性だけによって external に定式化することが可能なのです。次の定義を見てください。

7

定義 3.2 射 f : A → B について、(1) f がモニック（monic）であるとは、任意の射の組 g, h : C → A について、
f ◦g= f ◦h⇒g=hが成り立つことを言う。

(2) f がエピック（epic）であるとは、任意の射の組 g, h : B → C について、g◦ f =h◦ f ⇒g=hが成り立つことを言う。
射 f がモニックであるかエピックであるかは、 f と他の射との関係性だけによってきまります。ところが、次の事実を簡単に示すことができます：
命題 3.1 写像 f : A → B が Sets の射としてモニック（resp. エピック）であることと、写像として単射（resp. 全射）であることは同値。
つまり、単射性や全射性は、集合の中身に立ち入らなくても記述できる写像の性質だったのです。対象の中に立ち入らなくても意外とイケルぞ、という一例です。こうなったら external なやり方を貫いて、いけるところまで行ってみることにいたしましょう。
第２-３講のメイントピックは、普遍性（universal property）による対象の定義です。圏論の内部で、何か新しい対象を定義するときの一般的な方法論を紹介します。
ここでひとつ、非常に重要な概念を導入しておきましょう。
定義 3.3 圏 C の射 f : A → B に対して、ある射 g : B → A が存在してg ◦ f = 1A かつ f ◦ g = 1Bが成り立つとき、 f を同型（isomorphism）と呼ぶ。A から B への同型があるとき、A と B は互いに同型（isomorphic）であるといい、A  B と書く。
上の定義を見れば分かる通り、互いに同型な対象は external な立場からは区別がつきません。A  B のときには、A への射と B への射、A からの射と B からの射が１対１に対応してしまいますから、「外から見る限り」A と B の区別はつきません。
逆に言うと、射だけを見る圏論では、対象を同型を除いて（up to isomorphism）
区別するのが自然な立場になります。同型なものは同じと見做してしまうということです。ここは圏論的な考え方の、非常に重要なポイントです。

8それではいよいよ、圏論における対象の定義の仕方をご紹介しましょう。上でお話したとおり、圏の対象は up to isomorphism で定義されることになります。通常の数学で、新しい対象がどのように定義されてきたかを少し思い出してみてください。たとえば、２つの集合 A と B に対して、その積 A × B は、A の元 a と B の
元 b との順序づけられた組 (a, b) 全体のつくる集合、として定義されたのでした。
新しい集合を定義するために、その集合の元全体を、具体的に指定するわけです。
つまり、「中身が何か」を定義することによって、集合を定義しているわけですね。
集合は、その中身（元全体）によって特徴付けられるわけですから、当たり前と言えば当たり前です。
そうなると、中身に立ち入らない external なやり方で対象を定義するには、どうすればいいのでしょうか。対象と、対象の内部に立ち入るための所属関係（∈）によって構築される集合論に対して、圏論は、対象と、対象の間の射（→）によって成立しているのでした。この圏の世界では、対象は「中身が何か」（a ∈ A）ではな
く、「他の対象たちとどのように関係しているか」（ B → A）ということによって特徴づけられます。したがって、新しい対象を定義する際も、他の対象との関係
性のネットワークの中でその対象がどのような役割を果たしているのかを特定する必要があります。具体例として、先ほどの積の場合を考えてみましょう。
上でも述べたとおり、集合論的には、集合 A と B の積は、A の元 a と B の元 b との順序づけられた組 (a, b) 全体のつくる集合として定義されるのでした。今度は、
射の性質のみを使って、同じ対象を Sets の中で特定したいと思います。そのために、A × B が Sets の中でどのような「役割」を果たしているかを考察してみましょう。
まず、A× B からは、必ず A にも B にも射が伸びています。具体的には、π1 (a, b) =a, π2 (a, b) = b によって定義される、第１成分、第２成分への射影です。
π1

A.

π2

A ×.. B

B.

ただ、A にも B にも射があるという性質をみたす対象は Sets の中に他にいくらでもあるでしょう。それらの中で A × B はどのような意味で「普遍的」なのでしょうか。少し考察をしてみると、A × B というのは次の著しい性質を持っていることが分かります:

A.

f

X..

g

B.

というかたちの図式を任意に与えられたとき、次の図式が可換になるようなただひとつの射 u : X → A × B が存在する:

9

.

X.
f

A.

g

.∃!u
A ×. Bπ1

B.

π2

具体的には u(x) := ( f x, gx) によって u : X → A × B を定義すれば、上の図式が可換 4 になり、しかもそのようにして定義された u が上の図式を可換にするような唯一の射だ、ということが分かるでしょう。実は、この性質によって、A と B の積は同型を除いて一意的に決まってしまいます。
次の定義をみてみましょう。
定義 3.4 (積 product)
圏 C の対象 A, B についての積図式（product diagram）とは、対象 P と A, B から
なる図式
p1

A.

P..

p2

B.

であって、次の普遍写像性（Universal Mapping Property, 以下 UMP）を持つもののことを言う:
f

A.

X..

g

B.

というかたちの図式を任意に与えられたときに、次の図式が可換になるようなただひとつの射 u : X → P が存在する:

.

X.
f

A.

.∃!u
p1

P.

g

p2

B.

すなわち、 f = p1 u かつ g = p2 u．
ここでは上の考察にしたがって、A と B の積を具体的に構成する代わりに、A とB の積が「A にも B にも射が伸びているという性質を持つ対象の中で、最も普遍的なもの」として定義されているわけです。ここで「普遍的」と言っているのは、
図式が可換（commutative）であるとは「どの矢印を辿っても結果が同じ」ということです。上の図式の例で言えば、π1 ◦ u = f かつ π2 ◦ u = g というのが、可換性の意味です。これまでの数学では、関数による集合の元の振る舞いを「計算」していたわけが、圏論では可換図式（commutative
diagram）を使って射の振る舞いを「計算」します。
410

仮に別の対象 X が、同じように「A に向かっても B に向かっても射がある」という性質を満たしていたら、必ずその射は積 P を経由しますよ、ということです。
さて、このような定式化によって、確かに A と B の積が一意的（unique）に定まっていることを確認しましょう。
命題 3.2 上のようにして定義された積は、同型を除いて一意に定まる。
証明: 仮に、

A.

p1

P..

p2

q1

Q..

q2

B.

と

A.

B.

が共に A と B の積であったとしましょう。すると、まず Q が積であることから、ただひとつの射 i : P → Q が存在して q1 ◦ i = p1 , q2 ◦ i = p2 が成り立ちます。
同様に、今度は P が積であることから、ただひとつの射 j : Q → P が存在してp1 ◦ j = q1 , p2 ◦ j = q2 が成り立ちます。したがって、 p1 ◦ j ◦ i = p1 , p2 ◦ j ◦ i = p2
が分かります。ここで i, j がともに一意的に決まる射であったことから、 j ◦ i = 1Pが分かります。同様の議論により、i ◦ j = 1Q も言えて、したがって P  Q です。
□
積の定義によって A と B の積が同型を除いて一意に定まることが分かりました
ので、A と B の積が存在するとき、そのひとつを、A.

p1

A ×.. Bp2

B.

と書くことにしましょう（他にも無数にあるかもしれませんが、あったとしても所詮はこれと同型です）。そして、UMP によって誘導される u : X → A × B をこの場
合 < f, g > と書いて、これを f と g のペアリング（pairing）と呼ぶことにします。
以上のように、「かくかくしかじかのかたちをした図式の中で最も普遍的なもの」というかたちで対象を定義する方法を普遍写像性（Universal Mapping Property）
による対象の定義、と言います。以後、単に普遍性による対象の定義と言ったり、
UMP による定義と言ったりすることにします。具体的には上でも見たように、「他にもかくかくしかじかのかたちをした図式があったら、それは必ずこの図式を経由するよ」と言っているのが UMP です。この「普遍性」というのがいったい何のことを言っているのかは、次講の「極限と余極限」を学ぶことで見通しよく見え11

てきます。
ところで、上で定義したのは、２つの対象の間の積（binary product）でした。
まったく同様にして、n 個の対象の積も定義することができますが、それでは 0 個の対象の積とはなんでしょうか。積の UMP をよく見て、これを 0 個の対象の場合に当てはめてみると、次の定義が出てきます。
定義 3.5 （終対象, terminal object）
1 が圏 C の終対象（terminal object）であるとは、圏 C の任意の対象 C から 1 に、
ただひとつの射 !C : C → 1 が伸びてきていることを言う。
終対象とは 0 項積（nullary product）のことです。上の定義を見れば分かりとおり Sets の終対象は１点集合です。この終対象というのがこれまたとても大切な概念なのですが、それはまた追々、講義の中で触れていくことにしましょう。
講義ではこの調子で、普遍性によって定義できる圏論の重要な概念、終対象（terminal object）、始対象（initial object）、積（product）、余積（coproduct）、引き戻し（pullback）、押し出し（pushout）、イコライザー（equalizer）、コイコライザー（coequalizer）をそれぞれその例とともに紹介していきます。

第４講． 極限と余極限
第４講では極限（limit）と余極限（colimit）の概念を紹介します。ここで、第２３講で普遍性によって定義した対象たちが、どれも実は極限や余極限の例にほかならなかった、ということが判明します。「普遍性によって対象を定義する」というのは、極限や余極限として対象を定義するということだったのです。第２-３
講で扱ったすべての概念を吸収してしまうほど一般的な極限の概念ですが、実は、積とイコライザーがあれば、あらゆる極限がつくれてしまうことが分かります。講義では、この事実も証明します。
さらに、後半では関手（functor）と自然変換（natural transformation）の概念を導入し、特に表現可能関手（representable functor）が極限を保存することを確認します。ここまではずっと、ひとつの圏 C を固定してその中でいろいろと新しい対象を定義してきたわけですが、今度は一段視野を拡げて、圏と圏の間の関係性、
さらには圏と圏の間の関係性の間の関係性を記述する言葉を用意するわけです。それが、関手（functor）であり自然変換（natural transformation）です。講義で詳し
くお話しますが、ここでは定義だけ掲げておきます。

12

定義 3.6 （関手 functor）
F : C → D が圏 C から圏 D への共変関手（covariant functor）であるとは、F がC の対象を D の対象にうつし、C の射を D の射にうつす対応であって、以下をみたすものであることを言う：(a) F( f : A → B) = F( f ) : F(A) → F(B),(b) F(g ◦ f ) = F(g) ◦ F( f ),(c) F(1A ) = 1F(A) .
また、共変関手 F : Cop → D を、圏 C から D への反変関手（contravariant functor）という。ここで、Ob(Cop ) = Ob(C) で、C の射 f : D → C を圏 Cop の射 f : C → Dとする。つまり、Cop は圏 C の射をすべて形式的に逆向きにした圏で、これを Cの反圏（opposite category）と呼ぶ。
定義 3.7 (自然変換 natural transformation)
関手の組 F, G : C → D に対して、F と G の間の自然変換（natural transformation）
θ : F → G とは、圏 D の射の族

(θC : FC → GC)C∈C0
であって、圏 D の任意の射 f : C → C ′ に対して、θC ′ ◦ F( f ) = G( f ) ◦ θC が成り立つこと、すなわち以下の図式が可換になることを言う:

C.

FC
.

f .

Ff

C.′

FC
.′

θC

.
θC ′

GC
.
Gf

GC
.′

ここで θC を自然変換 θ の C でのコンポーネント（component）という。
圏 C から圏 D への関手を対象とし、その間の自然変換を射とする関手圏（functor
category）を DC と書くことにすると、θ : F → G が DC の射としてみて同型である
とき、θ を自然同型（natural isomorphism）と呼びます。自然変換が自然同型になる必要十分条件は、各コンポーネントが同型になることです。

13

第５講． 米田の補題
ここまで、圏論の external な視点ということを強調してきました。対象 A について考えるときに、A の中に立ち入る（a ∈ A）のではなく、A の外から A を見る（ B → A）のが、external な視点です。

A そのものを考える代わりに、A を外から見るというのは、圏論の言葉で言えば、
A 7→ HomC (−, A)という視点の変更を行うことだとも言えます。A そのものではなく、A に伸びてる射に注目しようということですね。ここで、Hom(−, A) と書いたのは、圏 C のそれぞれの対象 B に対して、Hom(B, A)、すなわち B から A への射の全体を対応させる関手のことです。
もう少しちゃんと書くと、局所小圏 C の任意の対象 A に対して、
関手 HA := HomC (−, A) : Cop → Sets を以下のように定義することができます:

B 7→ HomC (B, A)( f : B → B ) 7→ HA ( f ) : HomC (B′ , A) → HomC (B, A)
HA ( f )(g) := g ◦ f′

A が圏 C の対象だったのに対して、HomC (−, A) は圏 C から Sets への反変関手である、ということに注意してください。
C から Sets への反変関手を対象として、その間の自然変換を射とすれば、これはop圏になります。この圏を C 上の前層（presheaf）の圏と呼んで SetsC と書きます。
op
すると、A が C の住人だったのに対して、HomC (−, A) は SetsC の住人です。すな
わち、
A 7→ HomC (−, A)
opという視点の変更によって、背景の圏が C から SetsC に移行したわけです。実は、上の視点の変更そのものが、それ自身、ひとつの関手を定めます。
すなわち、以下のようにして関手 y : C → SetsC を定義することができます:op

A 7→ HomC (−, A)( f : A → B) 7→ y f : Hom(−, A) → Hom(−, B)yC (g) := f ◦ g

14

このようにして得られる関手 y が埋め込み（embedding）であること、すなわち、任意の局所小圏 C が C 上の前層の圏の部分圏として表現できるということを示すのが、米田の埋め込み定理（Yoneda’s Embedding Theorem）です。
米田の埋め込み定理:
op
任意の局所小圏 C に対して、上のようにして定義された関手 y : C → SetsC は埋め込み（すなわち、忠実、充満、かつ対象について単射）である。
この定理は、米田の補題（Yoneda’s Lemma）と呼ばれる以下の補題からただちにしたがいます。講義ではこの補題の証明を行います。
米田の補題:
局所小圏 C と C 上の任意の前層 P に対して、以下の自然な同型が存在する:

HomSetsCop (yC, P)  P(C)さて、米田の埋め込み定理により、

A 7→ HomC (−, A)という視点変更によって失われるものは何もない、ということが保証されます。失われるものが何もないどころか、得るところ実に大なのです。たとえば、局所小op
圏 C の中で射 A → B を探す代わりに、SetsC の中で対応する射 yA → yB を探せ
ばよい、ということになります。一般に、A → B を探すよりも yA → yB を探す方
opが容易な場合が多々あります。というのも、もとの圏 C に比べて前層の圏 SetsC
ははるかに「いい」性質（complete, cocomplete, cartesian closed, ...）を持っているからです。5前層の圏の持つ種々の性質については、次講であらためて詳しく解説をします。

op

第９講ではさらに、小圏 C に対しては、SetsC がトポス（topos）の構造をもつことを示します。トポスというのは、Sets と非常に似た豊かな構造を持つ圏です。
515

第６講． 前層の圏
op

第５講では、任意の局所小圏 C が C 上の前層の圏 SetsC に埋め込まれることをop確認しました。局所小圏 C の任意の対象 A は、HA := HomC (−, A) という、SetsCの対象として「表現」できるわけです。このような意味で、HA のことを表現可能
op
関手（representable functor）と呼びます 6 。SetsC は一般には、この表現可能関手
たちのまわりを、無数の表現可能でない前層たちが取り囲む、C よりもはるかに大きな圏です。
ところが C が小圏の場合、次の定理によって、実はあらゆる（表現可能とは限らない）前層たちが、表現可能関手の余極限として得られることが分かります。

∫
定理 3.1 C を小圏とする。このとき、C 上の任意の前層 P は、 J = C P を添字圏とする表現可能関手からなる図式の余極限 lim yC j  P として表せる。
−−→∫
ここで C P とは、P の要素の圏（category of elements）のことですが、詳細は講義で扱うことにしましょう。とにかく、表現可能関手たちこそが前層の基本的な構成要素（building block）である、ということを覚えておいてください。
さらに、次の事実も簡単に示すことができます。ただし、（余）完備（(co)complete）
な圏とは、すべての（余）極限が存在する圏のことです。
定理 3.2 局所小圏 C 上の前層の圏は完備（complete）かつ余完備（cocomplete）.
講義で詳細は確認しますが、(lim F j )(C) := lim(F jC), (lim F j )(C) := lim(F jC) と
←−−
←−−
−−→
−−→
pointwise に定義をすれば、これが前層の（余）極限を与えることが分かります。
op

第６講の後半では、局所小圏 C 上の前層の圏 SetsC がカルテシアン閉圏（cartesian closed category）になることを示します。そのためにまず、冪（exponential）の概念を導入します。

6

正確には、ある対象 A が存在して HA と同型になるような関手のことを表現可能関手と呼びます16

定義 3.8 （冪 exponential）
C を積を持つ圏とする。C の対象 C の B による冪（exponential）とは、対象 C Bと射 ϵ : C B × B → C であって、次の UMP をみたすもののことをいう:
任意の対象 Z と射 f : Z × B → C に対して、ただひとつの射 e
f : Z → C B が存在
して、ϵ ◦ ( ef × 1B ) = f となる。

C.B∃! f˜ .

Z.

ϵ

CB ×
. B

C.

.f

f˜×1B

Z ×. Bϵ : C B × B → C を evaluation と呼び、 f˜ : Z → C B を f の exponential transpose と呼びます。上の UMP により、以下の同型が得られます 7 。
HomC (Z × B, C)  HomC (Z, C B )f 7→ f˜ϵ ◦ g ←[ g
これでカルテシアン閉圏を定義する準備ができました。定義は単純明快です。
定義 3.9 （カルテシアン閉圏 cartesian closed category）
すべての有限積と冪を持つ圏のことをカルテシアン閉圏という。
シンプルな定義ですが、非常に重要な圏のクラスです。第 12 講で詳しくお話し
ますが、Curry-Howard-Lambek 対応によりカルテシアン閉圏は、直観主義命題論
理の自然演繹とも、型付 λ 計算とも見做せてしまうのです。第６講ではひとまず、
以下の定理を証明して終わる予定です。
op

定理 3.3 小圏 C 上の前層の圏 SetsC はカルテシアン閉圏である。
以上により、小圏 C 上の前層の圏は完備かつ余完備なカルテシアン閉圏であることが分かりました。

7

これは第７講で詳しく見るとおり、随伴の例になっています。

17

第７〜８講． 随伴
第７〜８講では、随伴（adjunction）の概念を導入します。随伴の概念は、圏論の中でも、最も重要な概念のひとつです。Robert Goldblatt は Topoi - the categoricalanalysis of logic の中で、 The isolation and explication of the notion of adjointness
is perhaps the most profound contribution that category theory has made to the historyof general mathematical ideas と書いています。第２-３講で導入した様々な概念
は、すべて（余）極限の概念に吸収され、さらにその（余）極限の概念は、随伴の概念に吸収されてしまいます。随伴というのはそれほどまでに一般的な概念であり、あらゆる分野の数学に遍在しています。
随伴には、互いに同値ないくつかの定式化がありますが、一番直観的に分かりやすいのは、次の定義でしょう（講義では、これと同値な別の定式化も紹介します）。
定義 3.10 （随伴 adjunction）
関手の組 F : C → D, U : D → C について、F が U の左随伴（left adjoint）、あるいは U が F の右随伴（right adjoint）であるとは、C ∈ C, D ∈ D に関する自然な同型

ϕ : HomD (FC, D)  HomC (C, UD)が存在することを言う。このとき、F ⊣ U と書き、組 (F, U, ϕ) のことを、圏 C と
圏 D の間の随伴（adjunction）と呼ぶ。
この定義から、ある関手の右随伴（もしくは左随伴）は、存在するとすれば同型を除いて（up to isomorophism）一意に決まることが分かります。実際、与えられた関手 F : C → D に対して、F ⊣ U かつ F ⊣ V だとすると、自然な同型
HomC (C, UD)  HomD (FC, D)  HomC (C, V D) が存在するので、米田の補題から直ちに、D についての自然な同型 UD  V D が出てきます。したがって、F ⊣ U かつ
F ⊣ V ならば U  V です。左随伴もまた同様の議論により、存在するとすれば一意であることが分かります。したがって、既知の関手の随伴として新たな概念を一意的に定義できる、ということになります。
随伴の定義によれば、F ⊣ U のとき、圏 D での FC から D への射と、圏 C でのC から UD への射が１対１に対応するのでした。このことを直観的に、

FC → D
C → UDと表現することにしましょう。このように書かれた場合、上の射と下の射が１対１に対応する、という意味だと思ってください。いくつか例を見てみましょう:18

(1) 対象が１つで射も１つ（恒等射のみ）の圏を 1 = {∗} と書くことにしましょう。このとき、任意の圏 C について、C から 1 へ射がただ１つ存在します。C
のすべての対象を ∗ に潰し、射を id∗ に潰す関手です。この関手を !C : C → 1と書くことにしましょう。このとき、関手 !C が右随伴を持つとはどういうことでしょうか？仮に !C ⊣ R となるような関手 R が存在したとしましょう。すると、次の１対１対応が存在することになります。
!C (C) → ∗C → R(∗)
さて、上の !C (C) というのは ∗ のことですから、改めて書きなおすと、次の１対１対応が分かります。

id∗ : ∗ → ∗C → R(∗)
この１対１対応により「C から R(∗) への射がただ１つ存在する」ということが分かります。任意の C に対してこれが成り立つわけですから、R(∗) は C の終対象ということになります。
以上により、!C が右随伴を持つということは、C が終対象を持つということにほかならない、ということが分かりました。同様に、!C が左随伴を持つという主張は、C が始対象をもつことと同値であることが分かります。

(2) 対角関手 ∆ : C → C × C を、∆(C) = (C, C)∆( f : C → C ′ ) = ( f, f ) : (C, C) → (C ′ , C ′ )により定義します。このとき、∆ が右随伴 R : C × C → C を持つとはどういうことでしょうか。仮にそのような R が存在したとすると、任意の C ∈ C と(X, Y) ∈ C × C について、以下の１対１対応があることが分かります:∆(C) = (C, C) → (X, Y)
C → R(X, Y)
すなわち、C から X への射と、C から Y への射の組に対して、C から R(X, Y)
への射がただ１つ自然に対応するというわけです。このことから、R(X, Y) 
X × Y 、すなわち ∆ ⊣ × という結論を導くことができます。この議論の双対（dual）を考えると、+ ⊣ ∆ が言えますから、併せて+⊣∆⊣×が成り立ちます。

19

(3) 積を持つ圏 C の A ∈ C に対して、積関手（product functor）−×A:C→C
を、対象については、

X 7→ X × A
射については、(h : X → Y) 7→ (h × 1A : X × A → Y × A)という対応を与えるものとして定義します。このとき、− × A が右随伴 R を持つとすると、以下の１対１対応が存在することになります。

X×A→Y
X → R(Y)
そこで、U(Y) = Y A , U(g : Y → Z) = gA : Y A → Z A と定めると、これが実際に− × A の右随伴を与えること、すなわち− × A ⊣ −Aとなることが確かめられます。
第６講で定義したカルテシアン閉圏とは、すべての有限積（すなわち終対象と積）と冪を持つ圏のことですから、以上の議論によってカルテシアン閉圏は随伴のみによって特徴付けが可能な圏である、ということが分かりました。
ところで、命題を対象と思って、命題間の帰結関係を射だと思うと、証明系は圏と見做せます。第 12 講で詳しくお話しますが、直観主義命題論理の自然演繹の体系は圏としてみるとカルテシアン閉圏になります（逆にカルテシアン閉圏を証明系とみなすと、直観主義論理の自然演繹に対応します）。実際、自然演繹における「かつ」の導入則、除去則はちょうど上で見た積の UMP と対応し、「ならば」の導入則はちょうど冪のところで見た exponential transpose に対応します。圏として見た自然演繹では「かつ」が積に、「ならば」が冪に対応するわけです。したがって「かつ」と「ならば」は（3）で見た随伴関係をみたすはずですが、これは任意の
命題 A, B, C に対して

A∧B⊢C
A⊢B⊃C
が成り立つということにほかありません。実際、上の証明図に相当する帰結関係を Π1 、下の帰結関係に相当する証明図を Π2 とすれば、以下のようにして、対応する下の証明図、上の証明図をそれぞれ作ることができます：

20

A

[B]1
(∧I)
A∧B
Π1
C
(⊃ I)1B⊃CA ∧ B (∧E)
A
Π2
B⊃C
C

A ∧ B (∧E)
B (⊃ E)「かつ」や「ならば」などの論理定項が随伴として特徴づけられるというのは、
驚くべきことではないでしょうか。実はこの考えはさらに推し進めることができて、量化子 ∃, ∀ もまた、随伴として理解できることが分かります。

(4) U =< A, . . . > を１階のモデルとして、たとえば φ(v1 , v2 ) を２つの自由変数を持つ論理式としましょう。このとき、φ によって次のような A2 の部分集合が定まります。
X = {(x, y) : U |= φ[x, y]} ⊆ A2
一方、論理式 ∃v2 φ, ∀v2 φ を考えると、これらはいずれも自由変数を１つだけもつ論理式で、それぞれ次のような A の部分集合を定めることが分かります。

∃ p (X) = {x : ある y が存在して (x, y) ∈ X} ⊆ A∀ p (X) = {x : 任意の y に対して (x, y) ∈ X} ⊆ A
p を第１成分への射影 p : A2 → A とすると、∃ p (X) はちょうど p による X の像 p(X) に対応しています。したがって、X ⊆ A2 , Y ⊆ A に対して、
X ⊆ p−1 (Y)∃ p (X) ⊆ Y
なる１対１対応が存在することが分かります。これは ∃ p ⊣ p−1 ということにほかなりません。
また、任意の x ∈ A に対して p−1 {x} = {(x, y) : y ∈ A} と書けますから、∀ p (X) = {x : p−1 {x} ⊆ X}と書けます。したがって、以下の１対１対応があることが分かります:p−1 (Y) ⊆ X
Y ⊆ ∀ p (X)
以上により、∃ p ⊣ p−1 ⊣ ∀ p となることが分かりました。

21

随伴の概念を媒介にして、ついに圏論と論理学が接近してきました。次講ではトポスの概念を導入して、もう少し圏と論理の関係を掘り下げてみることにしま
しょう。
ところで、
（１）と（２）によって始対象、終対象、積、余積のすべてが随伴によって特徴付けられることが分かったのでした。さらに次の例により、実はあらゆる（余）極限が随伴として特徴付けられることが分かります。

(5) 圏 C, D に対して、関手 ∆ : C → CD を以下のようにして定義する。
– 任意の X ∈ D0 に対して ∆(C)(X) = C– 任意の x ∈ D1 に対して ∆(x) = 1C .
このとき、lim ⊣ ∆ ⊣ lim .
−−→
←−−

22

第９講． トポス
冒頭から強調しているように、圏論には対象の元をとる（a ∈ A）という操作がありません。ところが、集合の元は１点集合からの写像と同一視できます。すな
わち集合 A の各元 a に、ā(∗) = a によって定まる写像 ā : 1 → A を対応させる同型A  HomSets (1, A)がありますから、これによって、A の元と１点集合から A の写像を同一視してしまうことができます。１点集合というのは Sets の終対象ですから、この状況を一般化して、次のように定義してみましょう。
定義 3.11 終対象を持つ圏 C の対象 A の点（point）8 とは、終対象から A への射のことを言う。
このように定義をすることで、普通の意味では点を持たない一般の圏にまで、点の概念を拡張することができます。ただし、このように点を定義すると、圏によっては、極端に点が少ない場合も考えられます。たとえば、モノイドとその間の準同型が成す圏 Mon を考えると、Mon では任意の対象が１点しか持たないことが分かります。したがって、Mon の中では、任意の射の組 f, g : M → N と任意の（というかそもそも１つしか存在しない）点 x : 1 → M について、 f x = gx が成り立ってしまうことになります。つまり、Mon の対象には射の違いを検出するのに十分なだけの点がないわけです。逆に、終対象をもつ圏 C が
任意の異なる射 f, g : A → B に対しある点 a : 1 → A が存在して f a , ga.
という性質をみたすとき、圏 C は well pointed であると言います。一般には、圏の対象は十分に多くの点を持つとは限りません。そのような場合には射の違いを検出するために、一般化された元（generalized element）を考える必要が出てきます。A の一般化された元とは単に、A を終域とする射のことです。
このようにして集合における元の概念は、射の言葉によって一般化することができます。次に、集合における「部分」の概念を、射の言葉に翻訳していくことを考えてみましょう。集合 A の元が１点集合からの写像の像と同一視できたのと同様に、A の部分集合は A への単射の像と同一視できます。集合における単射の概念は、圏論ではモノの概念に一般化されるのでした。そこで、次のように定義をしてみます。

global element という言い方をすることもあります。こちらの方が一般的かもしれませんが、いい和訳が思いつかないので、ここでは「点」の方を採用しました。
823

定義 3.12 圏 C の対象 A の部分対象（subobject）とは、モノ

m : M ,→ Aのことを言う。

A の部分対象 m と m′ の間の射 f : m → m′ を、次の可換図式によって定義します。
f

M.
m

M. ′
.

.

m′

X.

m′ はモノなので、上の図式を可換にする f は高々１つです。ここでm ⊆ m′ ⇔ ∃ f : m → m′
によって部分対象間の包含関係を定義します。さらに、互いに部分対象として同型な m と m′ を同一視することにすれば、A の部分対象たち全体 Sub(A) は、包含関係に関して poset の構造を持つことが分かります。
部分とはモノである、というのは部分を捉える１つの視点です。ここでは、もう１つの見方を検討してみましょう。集合 A の部分集合は、その特性写像（characteristicmap）によって特徴付けることができるのでした。集合 A の部分集合 U の特性写
像 χU : A → 2 とは{
1 (a ∈ U)
χU (a) =0 (a < U)
によって定まる写像のことです。
ここで、A の部分集合と特性写像の間の対応を圏論的に言い換えると、Sets では次の事実が成り立っているということが分かります。すなわち、対象 A の任意の部分対象 u : U ,→ A に対して、以下の図式を引き戻しにする射 χU がただひとつ存在する:

U.

!U

u

.

A.

χU

1.
true

2.

ただし、ここで true : 1 → 2 と書いているのは、t(∗) = 1 によって定まる写像のことです。この観察から、次のような一般化を考えてみることができそうです。

24

定義 3.13 E をすべての有限極限を持つ圏として１をその終対象とする。E の部分
対象分類子（subobject classifier）とは、対象 Ω と射 t : 1 → Ω の組であって、次の意味で普遍的な部分対象（universal subobject）になっているもののことを言う:
任意の対象 A とその部分対象 U ,→ A に対し、次の図式を引き戻しにする射χU : A → Ωがただひとつ存在する:

U.

!U

1.

u

.

t

A.

χU

Ω.

特に、終対象から部分対象分類子 Ω への射のことを真理値（truth value）と呼ぶ。
定義 3.14 すべての有限極限と冪を持ち、さらに部分対象分類子を持つ圏をトポス（topos）という。
これでようやく次の定理を証明する準備が整いました。
op

定理 3.4 小圏 C 上の前層の圏 SetsC はトポスの構造を持つ。
証明の概略:
op
第６講ですでに、任意の小圏 C に対して SetsC が完備なカルテシアン閉圏になる
op
ことを見ました。したがって、C が小圏の場合に SetsC が部分対象分類子を持つことを示せば十分ということになります。
まず、C の対象 C に対して、C を終域とする射全体の集合を S C と書いて、C 上の
total sieve と呼ぶことにします。その上で、右からの合成に関して閉じている S Cの部分集合を C 上の sieve と呼ぶことにして、前層 Ω をまずは対象に対して次のように定義します:Ω(C) := {S ⊆ C1 | S は C 上の sieve}
さらに h : D → C に対しては h∗ := Ω(h) : Ω(C) → Ω(D) を次のように定義します:h∗ (S ) := {g : · → D | h ◦ g ∈ S }このようにして定義された前層 Ω に対し、射 t : 1 → Ω の各コンポーネント
tC : 1 → Ω(C) を、tC (∗) = S C （C 上の total sieve）によって定義します。するopと、この t : 1 → Ω が SetsC の subobject classifier になることが分かります。
□

25

C 上の Sieve というのは、いわば C から見たときの真（true）になるまでの道のりです。Sets においては真理値が２つしかありませんでしたから、はじめから真であるか、あるいはもはや真になる道のりが存在しない（偽）かのいずれかです。
op
ところが、SetsC の場合には、肩に乗った C の分だけ圏に厚みがあります。いまopまで Sets では一切変動しない静的な集合を考えていたのに対して、SetsC の対象を考えることは、ちょうど C 上を変動する集合を考えていることに相当します。
結果として、C の厚みの分だけ、真理値にも厚みが出てきます。C の射を辿って真理（truth）に至るまでの様々な道のりがあり、その道のりの多様性の分だけ、真理値も多様になるわけです。

26

第 10 講． 命題論理のトポス意味論
第 10 講では、命題論理のトポス意味論を紹介します。ここでもまずは Sets の考察からはじめて、それを一般のトポスの場合に拡張していく方法をとることにしましょう。前講の最後でも強調したように、Sets というのは圏 1 上の前層の圏ですから、いわば変動しないトポス、静的なトポスです。この静的なトポスの上で成り立つ現象をまずはつぶさに観察して、それがトポスの場合にどのように一般化されていくのかを見ていくというのは自然な方法でしょう。
さて、Sets の任意の対象 X について、X の部分対象全体、すなわち X の冪集合
P(X) は包含関係に関して poset の構造を持ち、この poset は集合の演算によってブール代数の構造を持つのでした。

定義 3.15 （ブール代数, Boolean algebra）
ブール代数とは、元 0, 1 を持ち、二項演算 a ∨ b（join）、a ∧ b（meet）と一項演
算 ¬b（complementation）が定義されている poset であって、以下をみたすもののことをいう:0aa ≤ c and b ≤ cc ≤ a and c ≤ ba ≤ ¬b
¬¬a

≤
≤
iﬀ
iﬀ
iﬀ
=

a
1
a∨b≤c
c≤a∧b
a∧b=0
0

順序関係を射とみなすことで poset を圏と見れば、上の２つの条件は 0 と 1 がそれぞれ B の始対象、終対象であること、真ん中の２つの条件はそれぞれ積と余積のUMP にほかなりません。つまり、ブール代数とはすべての有限積と有限余積を持つ poset9 であって、さらに最後の２条件によって特徴づけられる一項演算（¬）を持つようなもののことです。集合の和をとる操作（∪）と共通部分をとる操作（∩）
をそれぞれ join と meet とし、補集合をとる操作（¬）を complementation とすれば、一般の冪集合が順序関係に関してブール代数の構造を持つことは明らかでしょう。もう１点付け加えておきますと、ブール代数の元 a, b に対して

ba := (¬a ∨ b)
によって冪を定義することができます。実際、evaluation ba ∧ a ≤ b の存在は、(¬a ∨ b) ∧ a = (¬a ∧ a) ∨ (b ∧ a) = 0 ∨ (b ∧ a) = b ∧ a ≤ b.
もっというと、任意の束（lattice）はすべての pullback を持つことが容易に証明できますので、ここからただちにブール代数はすべての有限（余）極限を持つことが分かります。
927

という簡単な計算によって確かめることができますし、冪の UMP、すなわち「a∧b ≤c ならば a ≤ cb 」ということも、以下の計算によって確認できます:a ≤ ¬b ∨ a ≤ (¬b ∨ a) ∧ (¬b ∨ b) = ¬b ∨ (a ∧ b) ≤ ¬b ∨ c = cb .
結果として、ブール代数は poset としてみたときに、カルテシアン閉圏の構造を持つことが分かりました。そこで、次のようにブール代数の概念を自然に一般化することができます。
定義 3.16 （ハイティンク代数, Heyting Algebra）
圏としてみてカルテシアン閉で、かつすべての有限余極限を持つ poset をハイ
ティンク代数と呼ぶ。
ハイティンク代数をカルテシアン閉圏と見たときの冪 ba を、以後 a ⇒ b と書くことにします。
ハイティンク代数だからといってブール代数であるとは限らないことに注意してください。実際、¬a := a ⇒ 0
によって a の complement を定義しようとすると（この定義はブール代数において ¬a = ¬a ∨ 0 = a ⇒ 0 が成り立つことから必然的に要請されます）、一般には¬¬a ≤ a が成り立つとは限りません 10 。たとえば、位相空間 X の開集合全体は包含関係に関してハイティンク代数の構造を持ちますが、このとき X の開集合 U について ¬U は X − U の内部になりますから、たとえば X として区間 [0, 1] をとれば、¬¬(0, 1) = [0, 1] となり、ただちに反例が得られます。実は、ブール代数が古典命題論理の（証明可能性の）意味論を与えるのと同様に、ハイティンク代数は直観主義論理命題論理の（証明可能性の）意味論を与えます。
さて、Sets の各対象 X の部分対象全体のなす poset Sub(X) が持つこの代数構造は、Sets の部分対象分類子 2 の代数構造に統制されています。２点集合 2 = {0, 1} に自然にブール代数の構造が入るのはみなさまよくご存知のとおりで、これが通常の古典命題論理の（証明可能性の）意味論を与えます 11 。Sets ではさらに、true : 1 → 2の持つこのブール代数の構造が引き戻される（pullback）かたちで、任意の対象 Xについて Sub(X) の持つ代数構造が定まります。ということは、一般のトポス E においても、E の部分対象分類子 t : 1 → Ω が何らかの意味で代数構造を持ち、そのこのため、¬a は a の擬補元（pseudo complement）と呼ばれます。
ここでは単に２点集合を考えているだけでなく、案に元 0 と 1 とを区別しています。すなわち、
0 と 1 のうちどちらが「真」を表すのかという情報込みで集合 2 を考えているわけです。1 が真を表しているということにすれば、これはちょうど 1 点を {0, 1} の中の 1 に移す 写像 true : 1 → 2 を考えていることに相当します。
10

11

28

構造が引き戻されることで、E の各対象 E の部分対象全体 Sub(E) がまた代数構造を持つことになるのではないかと予想されますが、実際そのとおりになります。順
を追ってみていくことにいたしましょう。
まず、集合 2 上に定義される真理関数（truth function）（¬）、（∧）、（∨）、（⇒）
を、それぞれ 2 への射として書きなおし、それによって真理関数の概念を一般のトポスへと拡張してみることにしましょう。

negation （¬）:¬ : 2 ⇒ 2 は、真理値を反転させる射ですが、これは部分集合 {x | ¬x = 1} = {0} ⊆ 2の特性関数 χ{0} のことにほかなりません:
!1

1.

1.

.

false

2.

true

2.

χ{0}

そこで部分対象分類子 t : 1 → Ω を持つ一般のトポス E においても、次の図式を引き戻しにする唯一の射として ¬ : Ω → Ω を定義することにします:
!1

1.
⊥

Ω.

1.

.

t

¬:=χ⊥

Ω.

ここで ⊥ は ! : 0 → 1 の特性関数とします。

conjunction （∧）:
射 ∧ : 2 × 2 → 2 による {1} の引き戻しは {(1, 1)} です。すなわち、以下が引き戻しの図式になります:
!1

1.

.

<true,true>

2 ×. 2

1.
true

∧

2.

そこで一般のトポス E においても、< t, t >: 1 → Ω × Ω の特性関数として ∧ :Ω × Ω → Ω を定義することにします。

29

implication （⇒）:⇒: 2 × 2 → 2 は、部分集合≤:= {(0, 0), (0, 1), (1, 1)} ⊆ 2 × 2の特性関数です。すなわち以下が引き戻しの図式になります:

≤.

!1

1.

.

true

2 ×. 2⇒2.

そこで、一般のトポス E においても、まずイコライザー

e

≤.

Ω×Ω

∧
p1

Ω

として e :≤,→ Ω × Ω を定義した上で、これの特性関数として ⇒: Ω × Ω → Ω を定義します。

disjunction （∨）:∨ : 2×2 → 2 は D := {(1, 1), (1, 0), (0, 1)} の特性関数です。そこで、A := {(1, 1), (1, 0)}, B :={(1, 1), (0, 1)} とおくと、D = A ∪ B で、以下の図式を考えると:2 +. 2

2.
<true,1>.f

2.
<1,true>

2 ×. 2.

f = [< true, 1 >, < 1, true >] で、Im f = D．したがって f は以下のように分解できます:f2 +. 2
f∗

D

30

2×2

そこで、一般のトポス E では ∨ : Ω × Ω → Ω を [< t, 1 >, < 1, t >] : Ω + Ω → Ω × Ωの像として定義します。
命題論理の E-意味論
以上、集合 2 上の真理関数（truth function）を 2 への射として特徴付けることによって、これを一般化して一般のトポス E の部分対象分類子 Ω 上の真理関数を得ることができました。これで、トポス E 上で命題論理を展開することができます。
トポス E の真理値とは射 1 → Ω のことをいうのでした。つまり HomE (1, Ω) が E の
真理値の集合です 12 。通常、古典命題論理の（証明可能性の）意味論をブール代数への付値（valuation）として与えることができたのと同様に、命題論理の E-意味論を、HomE (1, Ω) への付値（これを以下 E-付値と呼ぶ）として与えることができます。基本的な考え方は、通常の古典命題論理の意味論をブール代数への付値として与える場合とまったく同じで、命題変数全体 Φ0 上の付値 V : Φ0 → HomE (1, Ω)
は、

V(¬φ)
V(φ ∧ ψ)V(φ ∨ ψ)V(ϕ → ψ)

:=
:=
:=
:=

¬ ◦ V(φ)∧◦ < V(φ), V(ψ) >∨◦ < V(φ), V(ψ) >⇒ ◦ < V(φ)V(ψ) >とすることで論理式全体 Φ 上の付値 V : Φ → HomE (1, Ω) に一意的に拡張できます。ここで、任意の E-付値 V に対して V(φ) = t : 1 → Ω をみたすような論理式 φ
を E-妥当（E-valid）な論理式と呼んで E |= φ と書くことにすると、次のことはすぐに確かめることができます:
定理 3.5 E を任意のトポスとするとき、E |= φ なら ⊢CL φ．
ところが、一般に逆は成り立ちません。もう少し具体的に言うと、ある論理式 φが存在して E ̸|= φ ∨ ¬φ となるようなトポス E が無数に存在します。もう少し考察を進めてみましょう。

ここで、一般に HomE (1, Ω) は E の対象であるとは限らないということに注意してください。
Ω  Ω はもちろん E の内部の対象ですが、HomE (1, Ω) は圏 E の外部にあります。E から見たら部外者です。これがあとで微妙な問題を引き起こすことになります。
12

1

31

Sets では任意の対象 X について Sub(X) が集合 2 によって統制された代数構造を持つのでした。つまり:
命題 3.3 A, B をそれぞれ特性関数 χA : X → 2, χB : X → 2 によって定まる X の部分集合とすると、(1) χ¬A = ¬ ◦ χA(2) χA∩B = ∧◦ < χA , χB >(3) χA∪B = χA ∪ χB
この事実を一般化して、トポス E の対象 E についても Sub(E) 上の演算（¬）、（∩）、（∪）をそれぞれ以下のようにして定義することができます:• complement
f : A ,→ E に対して f の complement¬ f を特性関数 ¬ ◦ χ f によって、すなわ
ち t : 1 → Ω の ¬ ◦ χ f による引き戻しとして定義する:
¬A
.

!A

¬f

.

t

¬◦χ f

Ω.

E.

1.

すると、定義から χ¬ f = ¬ ◦ χ f ．

• intersection
f : A ,→ E, g : B ,→ E に対し、その intersection f ∩ g を t : 1 → Ω のχ f ∩ χg := ∩◦ < χ f , χg > による引き戻しとして定義する:!A∩B

A ∩. Bf ∩g

E.
すると、χ f ∩g = χ f ∩ χg ．

32

1.

.

t

χ f ∩χgΩ.

• union
同様に、χ f ∪g = χ f ∪ χg となるように、 f ∪ g を t : 1 → Ω のχ f ∪ χg := ∪◦ < χ f , χg > による引き戻しとして定義する。
以上の準備のもとで、次の定理が成り立ちます:
定理 3.6 トポス E の任意の対象 E について、(Sub(E), ⊆) はハイティンク代数の構造を持つ。
一般に集合の冪集合が、集合 2 によって統制されたブール代数の構造を持っていたのと同様に、任意のトポスはその部分対象分類子によって統制された構造を持つことが分かりました。しかし、それは一般にハイティンク代数にはなります
が、ブール代数になるとは限りません。Sets の自然な一般化のように見えるトポ
スですが、トポスに備わっている論理は一般に古典論理ではなく、直観主義論理なのです。古典論理の現象を圏論的に再構成してみたら、自然に出てきた論理は直観主義論理だったわけです。
ところで、任意の対象 E について (Sub(E), ⊆) がブール代数の構造を持つようなト
ポス E のことをブールトポス（Boolean topos）と呼びます。ブールトポスについては、以下が成り立ちます:
定理 3.7 E がブールトポスのとき、任意の論理式 φ に対して E |= φ ∨ ¬φ．
ところが、不思議なことに、逆は一般には成り立ちません。たとえば２元からなる
モノイド M2 から集合への M2 -作用全体がなすトポス M2 を考えると、M2 はブールトポスでないにも関わらず、M2 |= φ ∨ ¬φ が成り立ってしまうことが分かります。M2 の論理は internal には非古典的に振る舞うのに、外から見ると古典的に見えるのです。
どうしてこんなことが起こってしまうのでしょうか。実は p.31 の脚注でも触れたのですが、HomE (1, Ω) は一般に E の対象であるとは限りません。E の中から見たら HomE (1, Ω) は存在しないのです。そのようにして E の外部にある対象を使って付値 V : Φ → HomE (1, Ω) を定めたわけです。この付値そのものはいかなる意味
でも E の内部の射ではありません。そういう意味で、E |= φ ∨ ¬φ というのは、あくまで E を外から見たときに、E 上の論理が古典的に見える、ということを言っているにすぎません。

33

そこで、φ ∨ ¬φ を E の内部の言葉で言い直すとどうなるでしょうか。それは、以下の図式が可換になることと対応します。
!ΩΩ.
<1Ω ,¬>.

Ω ×. Ω

1.
t

∧

Ω.

実はこれはちょうど、トポスがブールトポスになる必要十分条件を与えます。
このように、トポスを外から見たときの論理的な振る舞いと、トポスを internalにみたときの振る舞いとは、一般に一致するとは限りません。トポスの内部に留まって数学を展開するのであれば、重要なのは後者の方ですが、外から見たトポ
スの論理的な振る舞いを見ることも、たとえば直観主義論理のモデルなどを考える際には、極めて重要な視点になります。13

本講のタイトルはもともと「トポスと論理」としていましたが、ここでやっていることは、基本的にはハイティンク代数の構造を持つ Sub(1) で命題論理を解釈するという、それだけのことです。したがって「トポスと論理」というタイトルはあまりにもミスリーディングであろうというご指摘を専門家からいただき「命題論理のトポス意味論」とタイトルを改めました。また、そもそも本稿に目を通してくださったトポスの専門家からは、本稿が専門家から見て（少なくともトポスに関する記述については）あまりにも視野の狭いものであるとのご指摘もいただいています。言葉の本来の意味で「トポスと論理」について講義をするのは、現時点での著者の力量を超えており、本稿があくまで「圏論入門」の講義の補助資料としてつくられたものであること、いかなる意味でもトポスと論理についての専門的な講義を意図して書かれたものではないこと、本稿筆者は決してトポスの専門家ではなく、専門家から見てトポスについての記述が「杜撰」であるとの指摘を受けているということを、ここに明記しておきます（もちろん筆者の力量の範囲内では最大限正確に書くことに努めております）。本稿に目を通してくださる（特に非専門家の）みなさまは、その点にご留意の上、トポス理論を本格的に学習される場合には、ぜひ専門書をご覧ください。
1334

第 11-12 講． Curry-Howard 対応と型付 λ 計算の圏論的意味論
前講でトポスを命題論理のモデルとして考えたときに着目していたのは、論理式の証明可能性（provability）であって証明（proof）そのものではありませんでした。実際、トポスにおいて論理式の振る舞いをモデル化していたのは Sub(E) という poset でしたから、そもそも対象間に高々１つの射しかなく、論理式間の導出
関係は記述できても、証明そのものの違いを検出することはできません。ところが、近年の計算機科学の発達により、証明可能性だけでなく、証明そのものの持つ構造、ないしは（Curry-Howard 対応によって示唆される）証明の持つ計算的内容（computational content）を抽出したり理解したりすることが重要な意味を持つようになってきています。そこで本講では「証明の意味論」のひとつの例として、
カルテシアン閉圏による直観主義論理の意味論のお話をいたします。

Curry-Howard 対応
Curry-Howard 対応とは、関数型プログラミング言語の基盤でもある型付ラムダ
計算と、証明の形式体系である自然演繹の間の対応関係のことであり、本質的にはブラウワー、ハイティンク、コルモゴロフらによる直観主義論理のいわゆる BHK
解釈にまでその起源を遡ることができます。この対応により、自然演繹における論
理式は型付ラムダ計算における型に対応し、自然演繹における証明は型付ラムダ
計算におけるラムダ項（プログラム）の概念に相当することが分かります。
「証明」と「プログラム」という一見まったく違った現象が、Curry-Howard 対応を介してきれいに対応してしまうというのは、実に不思議 . . . なのでしょうか。Curry-Howard
対応とはどのような対応で、それが果たしてどれくらい不思議なことなのか、本講で考察をしてみることにします。
自然演繹（natural deduction）
ここでは直観主義命題論理の自然演繹の {∧, ⊃}-断片（以下 NJ({∧, ⊃})）を導入します。論理式 A が仮定 A1 , . . . , An から証明できる、ということを以下の推件（sequent）
によって表します:A1 , . . . , An ⊢ A
論理式の有限集合を表すのに Γ, ∆, . . . などの記号を用い、Γ, A と書いたら Γ ∪ {A}を意味することにします。NJ({∧, ⊃}) の推論規則は以下のように与えられます:35Γ, A ⊢ A(Id)

Γ ⊢ A1
Γ ⊢ A2(∧ intro)Γ ⊢ A1 ∧ A2

Γ ⊢ A1 ∧ A2(∧ elimi )Γ ⊢ AiΓ, A ⊢ B(⊃ intro)
Γ⊢A⊃B

Γ⊢A⊃B
Γ ⊢ A (⊃ elim)Γ⊢B

上記の推論規則を組み合わせることにより、たとえば以下のような論理推論を行うことができます:

(Id)
(Id)
A ∧ B ⊢ A ∧ B (∧ E)
A ∧ B ⊢ A ∧ B (∧ E)
A∧B⊢ BA ∧ B ⊢ A (∧ I)
A ∧ B ⊢ B ∧ A (⊃ I)⊢ A∧B⊃ B∧A
このように推論規則を組み合わせてできる木構造を証明図（proof figure）と呼んだり、あるいは単に証明（proof）と呼んだりします。
さて、本講冒頭でも強調したとおり、ここでの私たちの関心は証明そのものの持つ構造です。特に、直観主義論理のような構成的（constructive）な論理を考える上では、証明可能性のみならず、その証明の構成そのものが重大な関心の的になってきます。そこで、推件の中でも、その証明についての情報を明記することにしましょう。すなわち、 M が論理式 A の証明である、ということを意味する記法として M : A という書き方を導入して、いままで単に Γ ⊢ A と書いてきたところを、Γ ⊢ M : A と書くようにすることにします。するとたとえば、（∧）の導入則

Γ ⊢ A1
Γ ⊢ A2(∧ intro)Γ ⊢ A1 ∧ A2は、

Γ ⊢ M1 : A 1
Γ ⊢ M2 : A2(∧ intro)Γ ⊢ (M1 , M2 ) : A1 ∧ A2と書けて、これは「 M1 という A1 の証明（構成）と M2 という A2 の証明（構成）があるときに、その組 (M1 , M2 ) は A1 ∧ A2 の証明（構成）である」と読めますか
ら、これは「論理式 A1 ∧ A2 の構成とは論理式 A1 の構成と論理式 A2 の構成の組である」という BHK 解釈とちょうど対応します。同様に、（⊃）の除去則は

Γ⊢M:A⊃BΓ ⊢ N : A (⊃ elim)Γ ⊢ MN : B

36

と書けて、これもやはり「A ⊃ B の証明 M は、A の証明 N を B の証明 MN にうつす関数である」と読めば、まさに BHK 解釈そのものです。
さて、ここで、論理式をその証明によってラベル付けしたのと同様に、推件の仮定にもラベルを与えてみることにしましょう。たとえば

x : A, y : B ⊢ x : Aという具合です。その上で、（⊃）の導入則を書き下してみると

Γ, x : A ⊢ M : B(⊃ intro)Γ ⊢ λx.M : A ⊃ B
x によってラベル付けされた仮定 A の下で B の証明 M が得られたならば、A ⊃ Bの証明がある、というわけです。この証明の名前を λx.M と書くことにしたのは、当然、型付ラムダ計算との関係を意識してのことです。
ラムダ計算（lambda calculus）
定義 3.17 可算無限個の変数 x, y, z, . . . が与えられているとする。このとき λ 項（λterm）を以下の BNF(Backus-Naur Form) によって定義する:

M, N ::= x | (MN) | (λx.M)
λ 項の構成 (λx.M) を x に関する M の関数抽象（functional abstraction）と呼んで、(MN) を M の N に対する関数適用（functional application）と呼びます。λ 項とは、変数に関数抽象と関数適用を繰り返していくことで得られる式のことです。
素朴には、たとえば λx.x と書いたら、 x を入力したら x 自身を返す関数を表していると思ってください。すると当然 λx.x と λx′ .x′ は本質的に同じ関数を表していることになりますから、このように変数を互いに取り替えただけの λ 項は同一視します。14

λ 項 M の自由変数の集合 FV(M) を以下のように定義します:
FV(x) :≡ {x}FV(MN) :≡ FV(M) ∪ FV(N)FV(λx.M) :≡ FV(M)\{x}

本来ならば α 同値という概念を定義して、互いに α 同値な λ 項を同一視する、という説明の仕方をするのですが、煩雑になるためここでは省略します。
14

37

その上で、λ 項 M の自由変数 x への λ 項 N の代入を次のように定義します:N if y = x
y[N/x] :≡ 
y if y , x(MP)[N/x] :≡ (M[N/x])(P[N/x])(λy.M)[N/x] :≡ λy.(M[N/x])
x , y, y < FV(N)定義 3.18 λ 項の β 変換 −→β を次のように再帰的に定義する:(1) (λx.M)N −→β M[N/x].
(2) M −→β N ならば， λx.M −→β λx.N ， MP −→β NP，PM −→β PN ．
function とは何かというところから、圏の概念を導入した本稿ですが、ラムダ計算もまたひとつの強力な function の理論です。ただし、ここではご覧のとおり、function は始域や終域という概念から解放されています。ここでλ式と言われているものは（A → B）ではなく、いわば純粋な（→）、始域や終域という制約から解放された純粋な function としての規則そのものです。始域や終域という制約が外されていることによって、かなり思い切った操作も許容されます。たとえば、λ 項を λ 項自身に適用する、というようなことも可能です。ここでたとえば、
ω = λx.xx を考えてみると、ωω →β ωω →β ωω →β . . . となってしまい、計算が止まりません。
そこで、λ 項に型（type）の概念を導入して、λ 項にも始域と終域に相当する制約を付加することにしたらどうなるでしょうか。興味深いことに、この制約を加えると、λ 計算がちょうどカルテシアン閉圏と対応し、２つの function の理論が奇しくも出会いをはたすことになります。
単純型付ラムダ計算（simply typed lambda calculus, STLC）

定義 3.19 可算無限個の変数 x, y, z, . . . と型変数 b, . . . が与えられているとする。このとき単純型付ラムダ計算（以下 STLC）を次の BNF によって定義する:
型 : A, B ::= b | A ⇒ B | A × B

λ項 : M, N ::= x | < M, N > | πi (M) | λxA .M | (MN)
ここで λ 項の型付け規則（typing rule）を導入します。M : A と書いたら「λ 項は型
A を持つ」という意味を表すことにします。λ 項の型付け規則は型判定式（typing
judgment）によって与えられます。型判定式は、以下のようなかたちの列のことをいいます:

x1 : A1 , x2 : A2 , . . . , xn , An ⊢ M : A
38

左辺の x1 : A1 , x2 : A2 , . . . , xn , An を型環境（typing context）と呼んで記号 Γ などを使って表します。型環境には同じ変数が２回以上あらわれることはないと仮定しておきます。以上の準備の下、STLC の型付け規則は以下のようにして与えられます:Γ, x : A ⊢ x : AΓ ⊢ M1 : A1
Γ ⊢ M2 : A2
Γ ⊢ (M1 , M2 ) : A1 × A2

Γ ⊢ M : A1 × A2
Γ ⊢ πi (M) : Ai

Γ, x : A ⊢ M : BΓ ⊢ (λxA .M) : A ⇒ B

Γ⊢M:A⇒BΓ⊢N:AΓ ⊢ (MN) : B

上の型付け規則によって型判定式 Γ ⊢ M : A が導出可能なとき、項 M は型付け可能（typable）であるといいます。またラムダ計算のときと同様、STLC の β 変換を定義します。
定義 3.20 型付 λ 項の β 変換 −→β を次のように再帰的に定義する:(1) (λx.M)N −→β M[N/x]， πi (M1 , M2 ) −→β Mi .
(2) M −→β N ならば， λx.M −→β λx.N ， MP −→β NP，PM −→β PN ．
直観主義論理の自然演繹の（∧, ⊃）-断片との対応関係は明らかですね。自然演繹における論理結合 ∧, ⊃ がそれぞれ、STLC の型コンストラクタ ×, ⇒ と対応し、さらに、自然演繹の論理式が STLC の型に、自然演繹の証明が STLC の項にそれぞれちょうど対応しています。
さらに、上で定義した β 変換はラムダ計算の非常に重要な概念です。β 変換こそが、計算のダイナミクスを担っているからです。β 変換は、自然演繹の何に対応するのでしょうか？すなわち、証明の中にあるダイナミクスとは、何なのでしょうか？実は、
β 変換にちょうど対応するのが、自然演繹における証明の正規化（normalization）
であるということが分かります。すなわち、証明の回り道（detour）の除去こそが、証明の中のダイナミクスなのです。
ここまで来ると、Curry-Howard 対応の背景にカルテシアン閉圏が見えてきたのではないでしょうか。その対応を見ていく前に、η 変換と λ 同値の概念を導入してお
きます。

39

定義 3.21 −→β によって定まる同値関係を =β と書いて M =β N となるとき、 M とN は互いに β 同値であるという。さらに、

M =η λx.Mx
M =η (π1 M, π2 M)

x < FV(M)によって定まる同値関係 =η を定義して、=λ を =β ∪ =η が定める同値関係として定義する。
このとき、M =λ M ′ の導出に関する帰納法によって、次のことが確かめられます:
命題 3.4 Γ ⊢ M : A かつ M =λ M ′ ならば、Γ ⊢ M ′ : A．

カルテシアン閉圏による STLC の表示的意味論
第 12 講ではカルテシアン閉圏による STLC の表示的意味論（denotational semantics）を紹介します。具体的には STLC の型判定式 x1 : A1 , . . . , xn : An ⊢ M : B がカルテシアン閉圏 C の射

JA1 K × . . . × JAn K → JBKと対応するように、STLC を C の中で解釈する関数 J−K を定義していきます。
定義 3.22 C をカルテシアン閉圏として、STLC の各型変数 b に対応する C の対象b̃ が与えられているとする。このとき、STLC から C への解釈関数 J−K を型と型付 λ 項に対して、次のように再帰的に定義する:

JbK := b̃, JA × BK := JAK × JBK, JA ⇒ BK := JAK ⇒ JBK
πi

Jx1 : A1 , . . . , xn : An ⊢ xi : Ai K := JA1 K × . . . JAn K → JAi K
JΓ ⊢ M : A ⇒ BK := fJΓ ⊢ N : AK := g

< f,g>

ev

JΓ ⊢ (MN) : BK := JΓK → (JAK ⇒ JBK) × JAK → JBKJΓ, x : A ⊢ M : BK := f : JΓK × JAK → JBKJΓ ⊢ (λxA .M) : A ⇒ BK := Λ( f ) : JΓK → (JAK ⇒ JBK)JΓ ⊢ M : A1 × A2 K := f : JΓK → JA1 K × JA2 K
fπiJΓ ⊢ πi (M) : Ai K := JΓK → JA1 K × JA2 K → JAi K
40

JΓ ⊢ M : AK := f : JΓK → JAKJΓ ⊢ N : BK := g : JΓK → JBKJΓ ⊢ (M, N) : A × BK :=< f, g >: JΓK → JAK × JBK
講義ではまず、この解釈が健全（sound）であること、すなわち、

M =λ N ⇒ JMK = JNKを示した上で、このように定義された解釈が完全（complete）となるようなカルテシアン閉圏 Cλ を具体的に構成してみるところまで進む予定です。詳細は当日の配布資料をご覧ください。

Curry-Howard 対応再考
講義では直観主義命題論理の自然演繹の（∧, ⊃）断片に関する Curry-Howard 対応を紹介しましたが、これは自然に（∨）を含む場合の直観主義命題論理、さらには（⊃）以外の論理定項（∨）、（∧）、（∃）、（∀）をすべて含む直観主義一階述語論
理および直観主義算術の全体にまで拡張されます。
計算体系にはラムダ計算以外にも様々なものがあります。ラムダ計算においては、
束縛変数の扱いがやっかいです。そこでラムダ抽象を捨てることで束縛変数の問題を回避するコンビネータ論理（combinatory logic）がありますが、実は、ラムダ抽象を用いないことが、ちょうど「ならば」の導入則を公理に置き換えることに対応して、結果としてコンビネータ論理における項はヒルベルト流の証明と対応することが分かります。ゲンツェンの推件計算（sequent calculus）に対応する計算体系の研究も行われていますし、個々の対応はあくまで証明系に依存したものであるとはいえ、Curry-Howard の対応は、そうした証明系の選択には依存しない、何かより本質的な「対応」を示唆しているようにも思えます。
しかし、本稿で紹介をした自然演繹とラムダ計算の対応も、もともとは直観主義
論理の BHK 解釈の中にある意味ですでに内包されていたとおり、広範に見えるこ
うした「対応」も、結局は直観主義論理の構成性と計算の構成性という、あまりにも素朴な対応を言っているにすぎないような気もしてきます。実際、1990 年までは「Curry-Howard 対応の古典論理版はない」と一般には信じられていたそうです [5]。ところが、1990 年に Timothy Griﬃn によって、ラムダ計算に継続呼び出し
演算子を加えることが直観主義論理に背理法を加えることに相当するという驚くべき結果が明らかになりました。「対応」は、古典論理にまで拡張されるのです。

41

参考文献
[1] S. Awodey．Category Theory．Oxford University Press，2006．
[2] R. Goldblatt．Topoi the Categorical Analysis of Logic (revised ed.)．Dover Publications，2006．
[3] C. McLarty．Elementary Categories, Elementary Toposes．Oxford University
Press，1992．
[4] J. Lambek and P. J. Scott．Introduction to higher order categorical logic．Cambridge University Press，1986．
[5] M. H. Sorensen and P. Urzyczyn．Lectures on the Curry-Howard Isomorphism．
Elsevier B. V. ，2006．
[6] S. Mac Lane and I. Moerdijk．Sheaves in Geometry and Logic a first introduction
to topos theory．Springer-Verlag New York，1992．
[7] S. Mac Lane．Samuel Eilenberg and categories．Journal of Pure and Applied Algebra，168(2-3)S:127-131，2002．
[8] S. Abramsky and N. Tzevelekos．Introduction to Categories and Categorical Logic．
New Structures for Physics．Springer，2010．
[9] 照井一成、「計算と論理」（『論理の哲学』第７章）、講談社選書メチエ、2005．
[10] 高橋正子、『計算論 計算可能性とラムダ計算』、近代科学社、1991．

本稿執筆にあたっては、多くのテキストやレクチャーノートを参考にさせていただきました。
そのすべてを挙げることはできませんが、そのなかでも特に参考にしたものをここに挙げました。
前半の、圏論の基礎的な内容については、[1] を特に参考にしました。また、第 9,10 講の内容は [2]を特に参考にしています。Curry-Howard 対応については [9] に大いに刺激され、執筆にあたっては[8], [5] を特に参考にしました。
1442