「型理論周辺、何で混乱するのか？」において：
型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです
地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\vdash`$'、二重矢印 '$`\Rightarrow`$'、上段・下段を区切る横棒などの記号が多義的に使われ、その意図・意味・使用法が読み取りにくいことがあります。
型理論の判断〈judgement〉に使われるターンスタイル記号と、演繹系〈演繹システム〉に対するメタ命題で使われるターンスタイル記号と、シーケント計算のシーケント区切り記号として使われるターンスタイル記号では、その意図・意味・使用法が違います。違い・区別をハッキリ認識しないと混乱してシッチャカメッチャカになります。
この記事では、メタレベルで使う非形式的な記法としてシーケント記法を導入します。シーケントの意味はメタレベルの命題と解釈します。最初の4つの節では、一般的な準備と注意事項を書きます。最初の4つの節だけでもそれなりの意味はあるかと思います。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mbb}[1]{ \mathbb{#1} }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in }}
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\LImp}{ \Longrightarrow}
\newcommand{\ctxpair}[2]{ \begin{pmatrix}#1 \\ #2\end{pmatrix} }
%\newcommand{\mapsot}{\style{display: inline-block; transform: rotate(180deg)} {\mapsto} }
%\newcommand{\vin}{ \style{display: inline-block; transform: rotate(-90deg)}{\in} }
\newcommand{\fibot}{\twoheadleftarrow}
\newcommand{\fibto}{\twoheadrightarrow}
\newcommand{\Rule}{\rightrightarrows}
%
\newcommand{\WF}{\mathbf{WF} }
\newcommand{\tot}{\mathbf{tot} }
\newcommand{\loc}{\mathbf{loc} }
\newcommand{\base}{\mathbf{base} }
\newcommand{\sect}{\mathbf{sect} }
`$
内容：
シーケント形式
判断にしろシーケントにしろ、次の形式〈フォーム | フォーマット〉をしています。
左辺 区切り記号 右辺
区切り記号としては、'$`\to`$'、'$`\Imp`$'、'$`\vdash`$' などが使われます。'$`\to`$' は圏論で多用されるし、'$`\Imp`$' は論理の含意記号として使いたいので、区切り記号は '$`\vdash`$' とします。
左辺と右辺には、なんらかの構文的対象物〈syntactic object〉を配置します。なんらかの構文的対象物を表わすメタ変数として $`A, B, A_1, A_2`$ などを使います。すると、判断／シーケントの基本形式は次の3種になります。
- $`A \vdash B`$
- $`\vdash A`$
- $`A_1, \cdots, A_n \vdash B`$
二番目の形式は左辺に何も書きません。右辺に何も書かないことを認めることもあります（例えば、ゲンツェンのLKシステム）が、ここでは認めません。右辺には、必ずひとつの構文的対象物を書きます。
三番目の形式が一般形式〈{general | generic} form〉であり、$`n = 1`$ とすると一番目の形式で、$`n = 0`$ とすると二番目の形式です。
今紹介した形式（書き方の方式・流儀）をシーケント形式〈sequent form〉と呼ぶことにします。シーケント形式は（今のところ）ほんとに形式〈フォーム | フォーマット〉であって、意図・意味・使用法については今は何も言ってません。
型理論ではシーケント形式を判断形式〈judgement form〉と呼びますが、ここでは「判断」ではなくて「シーケント」を採用しました。どちらの呼び名を採用するかは好みの問題です。強いて言えば、あとで導入する意図・意味・使用法が、どちらかといえば論理のシーケントに近いので、「判断」ではなくて「シーケント」を選んだ理由です。
命題としてのシーケント形式
自然演繹システムのような演繹システム〈演繹系〉を話題にして語るとき、対象とする演繹システムは形式化された命題（論理式）を内部に備えています。それと、演繹システムに関するメタな命題は別物です。対象物レベルの命題とメタレベルの命題の区別が必要です。
$`A, B, A_1, A_2`$ などは対象物レベルの命題を表わすメタ変数とします。前節のシーケント形式のひとつの使い途として、以下のような意味で使用することがあります。
- $`A \vdash B`$ ： 当該の演繹システムにおいて、$`A`$ を仮定して $`B`$ を証明可能である。
- $`\vdash A`$ ： 当該の演繹システムにおいて、何も仮定しないで $`A`$ を証明可能である。
- $`A_1, \cdots, A_n \vdash B`$ 当該の演繹システムにおいて、$`A_1, \cdots, A_n`$ を仮定して $`B`$ を証明可能である。
この意図・意味・使用法では、シーケント形式はメタ命題を表します。命題としてのシーケント形式を組み合わせて別なメタ命題が作れます。例えば、演繹定理〈deduction theorem〉として知られるメタ命題は次の形です。
$`\quad (A \vdash B) \Imp (\vdash A\Imp B)`$
さっそくに次の問題が現れました。
「型理論周辺、何で混乱するのか？」より：
文字・記号・語などが、対象言語（語るべき対象物である形式言語）のものか、記述言語（対象物を語るために使う言語）のものか紛らわしくなります。特に、ターンスタイル記号 '$`\vdash`$' や二重矢印 '$`\Rightarrow`$' が厄介です。
混同・誤認を避けるために、メタレベルで使う含意記号は“長い二重矢印”とすれば：
$`\quad (A \vdash B) \LImp (\vdash A\Imp B)`$
僕が個人的に使っている（けっこう便利な）方法は、メタレベルの論理記号を丸括弧で囲むものです。
$`\quad (A \vdash B) \;(\Imp)\; (\vdash A\Imp B)`$
実際には、対象物レベルの記号とメタレベルの記号を特に区別せず（同じ記号を使い）、文脈で適宜判断するというやり方が多数派でしょう。
規則は命題ではないのだが
規則と命題はまったく違うものですが、混同されることがあります。
簡単な事例から始めましょう。自然数 $`n`$ に対して後者自然数〈successor natural number〉（1 を足した自然数）を $`\mrm{succ}(n)`$ と書くことにします。以下の命題は真な命題です。
- $`0\in \mbf{N}`$
- $`n\in \mbf{N} \Imp \mrm{succ}(n)\in \mbf{N}`$
これらが命題である前提として、$`\mbf{N}`$ が既に存在する個別固有の集合であり、$`\mrm{succ}`$ も既に存在する個別固有の関数である、という事実があります。出てくる記号の意味が既に定まっているので、命題が言っている内容の真偽をうんぬんできるのです。
さて、ここからは、何もないところから新たに自然数の集合を作り出す行為を考えましょう。集合 $`\mbf{N}`$ がまだこの世に存在してない状況です。自然数達を作り出すには、次の帰納的構成規則を使います。
- ゼロは自然数である。
- $`n`$ が自然数ならば、$`n`$ の後者も自然数である。
- 以上により作られたモノだけが自然数である。
命題のときに使った $`0, \mrm{succ}`$ と区別するために、ゼロを表わす記号を $`\mrm{Z}`$ 、後者を表わす記号を $`\mrm{S}`$ とします。$`\mrm{S}`$ は事前に存在する関数の名前ではなくて、単なる記号です。プログラミング言語では、データコンストラクタ記号と呼ばれたりします。$`\mrm{Z},\mrm{S}`$ を使って帰納的構成規則を書き換えると：
- $`\mrm{Z}`$ は自然数である。
- $`n`$ が自然数ならば、$`\mrm{S}(n)`$ も自然数である。
- 以上により作られたモノだけが自然数である。
この規則により、$`\mrm{Z}, \mrm{S}(\mrm{Z}),\mrm{S}(\mrm{S}(\mrm{Z}) ), \cdots`$ が自然数であることが分かります。
まだ存在してないけど、作り出すべき集合として $`?N`$ という名前を使いましょう。先頭が疑問符なのは、まだ存在してないことを明示する目印です。未知の集合の名前 $`?N`$ を使って帰納的構成規則を書き換えると：
- $`\mrm{Z} \in {?N}`$
- $`n\in {?N} \Imp \mrm{S}(n)\in {?N}`$
- 以上を満たす $`{?N}`$ のなかで最小な集合が求めるべき集合である。
もし、まだ存在してない集合も $`\mbf{N}`$ という名前で呼び、$`\mrm{Z}, \mrm{S}`$ の代わりに $`0, \mrm{succ}`$ を使い、三番目の条件を省略してしまえば：
- $`0 \in \mbf{N}`$
- $`n\in \mbf{N} \Imp \mrm{succ}(n) \in \mbf{N}`$
冒頭に挙げた命題と見た目上はまったく区別が付きません。つまり、帰納的構成規則は、書き方によっては命題と判別できなくなるのです。しかし、見た目が同じだ（あるいは似てる）からといって、既存の集合・関数に関する命題と、まだ存在してない集合・関数を新しく作り出す帰納的構成規則をゴッチャにするのはとてもまずいことです*1。
推論規則
前々節に挙げた演繹定理（と呼ばれるメタ命題）を少し一般化すると次の形です。
$`\quad (A_1, \cdots, A_n, B \vdash C)\LImp (A_1, \cdots, A_n\vdash B\Imp C) `$
これをメタ命題と解釈するということは、既存の演繹システムがあって、その演繹システムにおいて真偽を判断できる、ということです。もし、上記メタ命題が成立するなら、その演繹システムでは「演繹定理が成立する」と主張できます。
それとは別な状況として、新しい演繹システムを構成するとき、$`A_1, \cdots, A_n, B \vdash C`$ となっているなら、$`A_1, \cdots, A_n \vdash B \Imp C`$ としよう、という規則を設定することができます。その規則を日本語で述べるならば：
- 我々の演繹システムにおいて、$`A_1, \cdots, A_n, B`$ を仮定して $`C`$ が証明できたとき、$`A_1, \cdots, A_n`$ を仮定して $`B\Imp C`$ を証明できたことにしよう。そう約束しよう。
この規則を、記号 $`\Rule`$ を使って以下のように書くことにしましょう。
$`\quad (A_1, \cdots, A_n, B \vdash C)\Rule (A_1, \cdots, A_n\vdash B\Imp C) `$
これは命題ではなくて推論規則〈inference rule〉です。推論規則は、帰納的構成規則の一種です。自然数達の集合がない状態から新たに定義するときに帰納的構成規則が使われたのと同様に、“証明された論理式達の集合”を新たに定義するときに推論規則（と呼ばれる帰納的構成規則）の集合が使われます。
形式文法〈formal grammer〉の生成規則〈production rule〉も帰納的構成規則の一種です。型理論や論理のなかでも文法の生成規則は使われます。推論規則も生成規則も帰納的構成規則だという点では同じですが、目的がまったく違います。困ったことには、推論規則と生成規則も混乱しがちなのです。
例えば、次の“規則”を考えましょう。
$`\quad (\vdash A, \vdash B)\Rule (\vdash A\land B)`$
推論規則として解釈するならば、その意図・意味は次のようです。
- 我々の演繹システムにおいて、$`A`$ が何の仮定もなしで証明できて、$`B`$ も何の仮定もなしで証明できたとき、何の仮定もなしで $`A\land B`$ を証明できたことにしよう。そう約束しよう。
しかし、'$`\vdash`$' を“構文的に許容できる”と解釈すると、次のようです。
- 我々の文法において、$`A`$ が構文的に許容できる論理式で、$`B`$ も構文的に許容できる論理式のとき、$`A\land B`$ も構文的に許容できる論理式としよう。
証明可能な論理式と構文的に許容できる論理式はまったく違います。例えば、以下の“規則”はどうでしょう。
$`\quad (\vdash A)\Rule (\vdash \lnot A)`$
推論規則としてはあり得ないものですが、文法の生成規則としては必要です。この生成規則がないと、否定の論理式を作れません。
型理論の習慣では、文法の生成規則（形成規則〈{formation | forming} rule〉と呼ぶ）と推論規則（相当の規則）も同じ判断形式で表わします。良くないと思いますが、言っても習慣が変わることはないです。
構文論的なモデル： 包括圏
ここから先で述べることは、「型理論周辺、何で混乱するのか？ 構文論的意味論と意味論的意味論」の分類で言えば、非形式的構文論的意味論〈informal syntactic semantics〉です。この意味論のモデルとは、型理論や論理の構文構造を圏論的に定式化した構文圏〈syntactic category〉です。
型理論、論理、そしてインスティチューション理論でも共通に使える構文圏として包括圏〈comprehension category〉を採用します。包括圏については以下の過去記事に書いています。
$`\pi:\cat{D} \to \cat{C}`$ を包括圏を構成するファイブレーション〈ファイバー付き圏〉とします。$`\cat{D}`$ がファイブレーションのトータル圏、$`\cat{C}`$ はファイブレーションのベース圏です。ベース圏 $`\cat{C}`$ の対象（型理論ではコンテキスト〈context〉と呼ぶ）は、大文字ギリシャ文字 $`\Gamma, \Delta, \Sigma`$ などで表します。
$`\Gamma\in |\cat{C}|`$ に対して、$`\Gamma`$ 上のファイバーを $`\cat{D}_{@\Gamma}`$ と書きます。ファイバーを局所圏〈local category〉とも呼びます。ローカル圏 $`\cat{D}_{@\Gamma}`$ の対象は、依存ペアを使って $`(\Gamma, A)`$ と書けます。依存ペアであることを強調するために、$`(\Gamma\mid A)`$ とも書きます。また、カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉の縦ベクトル記法も使います。
$`\quad \ctxpair{A}{\Gamma} = (\Gamma\mid A)`$
局所圏の対象は当然にトータル圏の対象です。トータル圏の対象は、どれかのベース対象（ベース圏の対象）上の局所圏の対象です。
包括圏は、コンテキスト拡張〈context extension〉と呼ばれる演算を持ちます。その演算は次のような関手です。
$`\quad (\cdot): \cat{D} \to \cat{C} \In \mbf{CAT}`$
$`(\cdot)`$ については「包括コンテキスタッドに向けて // 中置演算子記号の使い方」を見てください。
依存ペア $`(\Gamma \mid A)`$ ごとに、標準射影が決まります。標準射影は特別な矢印により明示します。
$`\quad \Gamma\cdot A \fibto \Gamma\In \cat{C}`$
標準射影のセクションの集合を次のように書きます。
$`\quad \mrm{Sect}_\cat{C}(\Gamma \fibot \Gamma\cdot A)\subseteq \cat{C}(\Gamma, \Gamma\cdot A)`$
双対的に、標準埋め込みのレトラクションも考えられますが、今日は触れません。セクションとレトラクションについては以下の過去記事を参照してください。
注釈付きターンスタイル
この記事で提案するシーケント形式は、包括圏に関する命題として解釈します。規則ではないので注意してください。シーケントの左辺と右辺の区切り記号はターンスタイル（'$`\vdash`$'）ですが、ターンスタイルがあまりにも多義的に使われて困惑するので、ターンスタイルの意図・意味・使用法を区別するための注釈として右肩にキーワードを添えます。そのキーワードを表にまとめます。
| キーワード | 意図・意味・使用法 | |
|---|---|---|
| WF（well-formed） | 整形式性（構文的に許容できること）を表わす | |
| tot（total） | トータル圏に関する命題に使う | |
| base | ベース圏に関する命題に使う | |
| loc（local） | ローカル圏に関する命題に使う | |
| sect（section） | ベース圏のセクションに関して使う |
注釈としてのキーワードが付いたターンスタイルの例を挙げると：
$`\quad \Gamma \vdash^\WF A`$
$`\quad \Gamma \mid A \vdash^\loc B`$
$`\quad (\Gamma\mid A) \vdash^\tot (\Delta \mid B)`$
シーケント形式の使用は非形式的です。つまり、シーケント形式を形式化した形式言語を含む形式体系〈formal system〉を考えるわけではありません。構文論的モデルである包括圏（前節参照）に対する圏論的命題の略記としてシーケント形式を使うだけです。
シーケント形式の解釈
包括圏を意味的対象物としての、シーケント形式の解釈（意図・意味・使用法）を示します。シーケントは、通常の圏論的命題と同義なので、左にシーケント形式、右に通常の命題の対応表で示します。
| $`\text{シーケント形式}`$ | $`\text{通常の書き方}`$ |
|---|---|
| $`\vdash^\WF\Gamma`$ | $`\Gamma\in |\cat{C}|`$ |
| $`\Gamma \vdash^\WF A`$ | $`A \in |\cat{D}_{@\Gamma}|`$ |
| $`\Gamma \mid A \vdash^\loc B`$ | $`\cat{D}_{@\Gamma}(A, B)\ne \emptyset`$ |
| $`\Gamma \mid A \vdash^\loc \varphi:B`$ | $`\varphi\in \cat{D}_{@\Gamma}(A, B)`$ |
| $`\Gamma \vdash^\base \Delta`$ | $`\cat{C}(\Gamma, \Delta)\ne \emptyset`$ |
| $`\Gamma \vdash^\base f:\Delta`$ | $`f\in \cat{C}(\Gamma, \Delta)`$ |
| $`(\Gamma\mid A) \vdash^\tot (\Delta\mid B)`$ | $`\cat{D}( (\Gamma\mid A), (\Delta\mid B) ) \ne \emptyset`$ |
| $`(\Gamma\mid A) \vdash^\tot F:(\Delta\mid B)`$ | $`F\in \cat{D}( (\Gamma\mid A), (\Delta\mid B) )`$ |
| $`\Gamma \vdash^\sect \Gamma\cdot A`$ | $`\mrm{Sect}_\cat{C}(\Gamma\fibot \Gamma\cdot A )\ne \emptyset`$ |
| $`\Gamma \vdash^\sect s:\Gamma\cdot A`$ | $`s\in\mrm{Sect}_\cat{C}(\Gamma\fibot \Gamma\cdot A )`$ |
ある程度の省略・略記はしても大丈夫ですが、安直に省略・略記するとワケワカランことになります。
まず、局所圏〈ファイバー〉にはそれぞれに終対象があると仮定して、それを次のように書きます。
$`\quad (\Gamma \mid 1) = \ctxpair{1}{\Gamma} = {_\Gamma 1} = 1`$
$`\Gamma \mid 1 \vdash^\loc B`$ を $`\Gamma \vdash^\loc B`$ と略記していいでしょう。対象システムが演繹システムなら、諸々の前提 $`\Gamma`$ から（明示的な仮定はなしで）命題 $`B`$ が証明可能だ、という解釈になります。
$`\Gamma \vdash^\sect \Gamma\cdot A`$ では、左右に同じ $`\Gamma`$ が登場するので、 $`\Gamma \vdash^\sect A`$ と略記したい気分になります。この省略を許すと、注釈以外は同じ形式が3つ生じてしまいます。
- $`\Gamma \vdash^\WF A`$
- $`\Gamma \vdash^\loc A`$
- $`\Gamma \vdash^\sect A`$
注釈を省略すると、どれのことかワケワカランことになります*2。型理論も論理も、このテの混乱の原因に無頓着で杜撰な傾向があります。「一切省略するな」とは言いませんが、他のシーケント形式と被らないように省略するのが無難で親切です。
もうひとつ許容できる（ときに有用な）省略があります。$`(\Gamma\mid 1) \vdash^\tot H:(\Delta\mid B)`$ を $`\Gamma \vdash H:(\Delta\mid B)`$ と省略してかまいません。これは、ベース対象 $`\Gamma`$ からトータル対象 $`(\Delta\mid B)`$ への射のように見えます。そのように見えてかまわないし、その解釈は（少なくともメンタルモデルとしては）役に立ちます（「型理論へのファイブレーション的アプローチ： インスタンスとは // ハープーン」参照）。
ここで導入した非形式的シーケント形式は、包括圏について語る言葉としてかなり便利です。通常の圏論の命題に翻訳できるので、無くても困ることはないのですが、将来的には形式化して、包括圏をモデルとする形式的体系に仕立てることが出来るかも知れません。
*1:[追記]とはいえ、混同してしまうのも無理もないことです。その事情について「型理論や論理における命題と規則： 混同する事情」に書きました。[/追記]
*2:逆に言えば、注釈を付けていれば区別できるということです。
