あっ、そうか！ と気が付きました。
型理論、圏論、集合論、論理などを一緒にやるときに、同義語・多義語に悩まされるのですが、記号に関しても同義記号・多義記号のカオス状態にストレスがたまります。
例えば、矢印記号に関しては次の過去記事に書いています。
上記過去記事の冒頭から、さらに11個の過去記事への参照があります。どの記事も、矢印記号の多義性に関する記事です。
今まで、特定の記号（例えば矢印記号）に注目して、その記号がどのように多義的に使われるかを説明していたのですが、発想を逆にして、特定の使用場面・使用意図のために、どのような記号が使われる可能性があるかを説明するほうが分かりやすいかも知れない、と思いました。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\dto}{\mathrel{!\!{\to}} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\id}{\mathrm{id} }
\newcommand{\cat}[1]{\mathcal{#1}}
%\require{enclose}
`$
内容：
グリフ
グリフ〈glyph〉とは、文字や記号の図形的な形状のことです*1。例えば、「コロン」「カンマ」「二重矢印」などのグリフはすぐに思い浮かべることができるでしょう。
コンピュータで使われる文字・記号には、すべてUnicodeの番号が振られています。名前も付いています。例えば、右向きの二重矢印記号ならば、番号が U+21D2 で、"RIGHTWARDS DOUBLE ARROW" という名前を持っています。「Unicode U+21D2」のような検索ワードでインターネット検索すれば、グリフを見ることも容易です。LaTeXで右向きの二重矢印記号を書きたいなら \Rightarrow として表示できます。
Unicode番号／Unicode名前、LaTeXコマンド〈制御シーケンス〉により記号を特定することができて、対応するグリフ（図形的な形状）は目視で確認できます。我々が目視で認識するのはグリフであって、Unicode番号／Unicode名前、LaTeXコマンドを意識している人は少ないでしょう。
ここで話題にするグリフは次のものです。右側にLaTeXコマンドを沿えておきます。
- $`:`$
: - $`\in`$
\in - $`\supset`$
\supset - $`\le`$
\le - $`\vdash`$
\vdash - $`\Vdash`$
\Vdash - $`\models`$
\models - $`\rightarrow`$
\rightarrow - $`\Rightarrow`$
\Rightarrow - $`\Rrightarrow`$
\Rrightarrow - $`\rightrightarrows`$
\rightrightarrows - $`\downdownarrows`$
\downdownarrows
グリフ（を持つ記号）には、Unicodeの名前以外に別名があります。例えば記号 '$`\vdash`$' は、Unicodeでは "RIGHT TACK" という名前ですが、よく知られた名前は「ターンスタイル〈turnstile〉記号」でしょう（「ターンスタイルって知っている？」参照）。"Right Tee" とも呼ぶようです。そして、LaTeXでは "vdash" です。
文字・記号は、グリフ（見た目）だけでなく意味を伴いますが、その意味は場面・意図（つまり文脈）により変わってしまいます。グリフに対して意味を固定的に考えるのではなくて、まず使用場面・使用意図を考えて、その場面・意図において使われるかも知れないグリフを知っておく、というアプローチが良さそうです。
使用場面・使用意図
前節に挙げたグリフ（を持つ記号）達が、どのような場面でどのような意図（目的）で使われるかを考えてみます。グリフそれ自体ではなくて、場面・意図に基づいて記号に名前を付けます。
- 含意〈implication〉記号（演算記号） ： 論理式または述語に対する“とある演算”を表す記号〈論理結合子記号〉
- エンテイルメント〈entailment | 伴意〉記号（関係記号） ： 論理式または述語のあいだの関係を表す記号。
- 導出可能性〈derivability〉記号（関係記号） ： 演繹系（後述）において、文（後述）が導出可能であることを示す記号〈メタレベルの記号〉
- 演繹ステップ〈deduction step〉区切り記号（ステップ構文の一部） ： 演繹系の演繹ステップの仮説〈前提〉と結論を区切る記号
- 妥当性〈validity〉記号（関係記号） ： モデルが文（論理式やシーケント）を満たす〈satisfy〉ことを示す記号（メタレベルの記号）
- 内部ホム〈internal hom〉記号（演算記号） ： 圏論における、対象・射に対する“とある演算”を表す記号
- 判断〈judgement〉区切り記号〈判断ストローク〉（判断構文の一部、多目的） ： 型理論において、様々な目的に使われる記号
- 所属〈membership〉記号（関係記号） ： 集合論の所属関係を表す記号
- 居住〈inhabitation〉記号（関係記号） ： 型理論の居住関係を表す記号
- プロファイル矢印（プロファイル構文の一部） ： 圏論のプロファイル（域と余域の仕様）記述で使う矢印記号
- プロファイルコロン（プロファイル構文の一部） ： 圏論のプロファイル記述で使うコロン記号
- パイ型構成〈Pi-type construction〉記号（演算記号） ： 依存型理論の集合論的解釈における、パイ型（と呼ぶ集合）を構成する演算を表す記号
文脈とグリフの関係
前節に挙げた文脈（使用場面・仕様意図）において、どのようなグリフ（を持つ記号）が使われる可能性があるかを列挙します。
- 含意 ： $`\supset, \to, \Rightarrow`$
- エンテイルメント ： $`\to, \Rightarrow, \vdash, \le`$
- 導出可能性 ： $`\vdash`$
- 演繹ステップ区切り ： $`\vdash, \rightrightarrows, \downdownarrows`$
- 妥当性 ： $`\models`$
- 内部ホム ： $`\to, \Rightarrow`$
- 判断区切り ： $`\vdash`$
- 所属 ： $`\in`$
- 居住 ： $`:`$
- プロファイル矢印 ： $`\to, \Rightarrow, \Rrightarrow`$
- プロファイルコロン ： $`:`$
- パイ型構成 ： $`\to`$
文脈とグリフに関して、以下に僕のコメントを書いていきます。
含意とエンテイルメント
エンテイルメントは伴意のことですが、「がんい」と「ばんい」または「はんい」は、口頭だと聞き間違いのリスクがあるのでカタカナで「エンテイルメント」にします。
含意とエンテイルメントはかなり混同されています。“演算”と“関係”だから全然違うのですが。記号もどちらも '$`\Rightarrow`$' で区別しない、なんてこともあります -- それはダメ！
僕は幸いにも、含意とエンテイルメントの混同をしたことはないのですが、それは最初に教わってから30年くらい（今は違うけど）次の記法を使い続けてきたからです。
- 含意記号は '$`\supset`$'
- エンテイルメント記号（シーケントの区切り記号）は '$`\to`$'
'$`\supset`$' が少数派でコミュニケーションに支障が出るので最近は含意に '$`\Rightarrow`$' を使っています。エンテイルメント記号は、圏論のプロファイル矢印とコンフリクトしますが、これはしょうがないです。昔は、エンテイルメント記号に '$`\vdash`$' を使うことがありましたが、型理論との記号の奪い合いの抗争に疲れたので、今は使いません（'$`\vdash`$' は型理論に譲った）。
述語と部分集合の一対一対応を強調するときは、エンテイルメント記号に '$`\sqsubseteq`$' を使うこともあります。対応する '$`\subseteq`$' と似てるからです。困ったことには、含意記号に相当する集合演算の記号がありません -- '$`\triangleright`$' とかを（テキトーに）使ってます。
導出可能性と妥当性
導出可能性記号は、演繹系に関するメタな記号です。演繹系については以下の過去記事を参照してください。
導出可能性は、演繹可能性〈deducibility〉とか証明可能性〈provability〉ともいいます。証明可能性をカタカナで「プロバビリティー」と言うと確率〈probability〉と区別が付かないので注意しましょう。
導出可能性〈証明可能性〉記号は '$`\vdash`$' 、妥当性記号は '$`\models`$' というルールは、論理・モデル理論では安定した習慣です。が、型理論では記号の奪い合いの抗争が勃発します。型理論では、演繹系の内部の記号（オブジェクトレベルの記号）として '$`\vdash`$' が出てきてしまうので、メタレベルの記号に '$`\vdash`$' を使うとひどく混乱します。
結局、'$`\vdash`$' は型理論の判断ストローク（判断の一部として使う記号）に譲って、導出可能性には '$`\Vdash`$' を使っています。'$`\Vdash`$' も内部（オブジェクトレベル）で使ってしまったときは '$`\Vvdash`$' 。
妥当性記号は型理論との抗争が起きないので安心して使えます。しかし、妥当性記号は論理的帰結〈logical consequence | 意味論的帰結 | semantic consequence〉の記号としてもオーバーロードされるので注意は必要です。
それと、演繹系に対するメタレベルの記号が、さらに形式化を重ねた上位の演繹系ではオブジェクトレベルの記号として使われることはしばしばあるので、これも要注意です。
演繹ステップ区切り
推論とか証明とか呼ばれる行為とそのメカニズムを抽象化した構造として演繹系〈{deductive | deduction} system〉があります（「演繹系とオペラッド」参照）。過去記事「演繹系とオペラッド」では、演繹系の内部で使う構文的対象〈syntactic object〉を「項〈term〉」と呼んでいたのですが、ここではインスティチューション理論にならって文〈sentence〉と呼ぶことにします。「文とは何か？」には答えず、演繹系を構成する集合 $`S`$ の要素だと位置付けます。
演繹系の演繹ステップ $`s`$ は、適当な自然数 $`n`$ に対して次のように書けます。
$`\quad s = ((s_1, \cdots, s_n), s_0) \in S^n \times S`$
$`n`$ 個の文の並び $`(s_1, \cdots, s_n)`$ がステップの仮説〈hypotheses | 前提〉で、$`s_0`$ が結論〈conclusion〉です。
ステップの仮説と結論を区切る記号は、長い横棒がよく使われます。仮説を上段に、結論を下段に書きます。この横棒は、LaTeX の bussproofs パッケージなどがないとうまく描けません。横向きに書くときに '$`\vdash`$ ' が使われることがあります。僕は、横棒の代替記号に '$`\downdownarrows`$' を使ってます。横向きに書くときは '$`\rightrightarrows`$' 。'$`\downdownarrows`$' と $`\rightrightarrows`$' の使用例は「球体集合達の圏の構文表示 2/2」にあります。
内部ホム
デカルト閉圏／モノイド閉圏には、内部ホム演算があります。一番よく使われる内部ホムの記号は $`[\hyp, \hyp]`$ でしょう。単なる矢印 '$`\to`$' も内部ホムの演算記号として使われることがあります。もちろん、プロファイル矢印とコンフリクトして具合が悪いですが。
論理をデカルト閉圏により定式化すると、論理の含意記号は内部ホムの記号に他なりません。この場合は、内部ホムの演算記号として '$`\Rightarrow`$' を使っているわけです。
折衷案により、内部ホムを $`[\hyp \to \hyp]`$ と書くのが良いだろうと思います。$`[\hyp, \hyp]`$ 派でも $`\hyp\to \hyp`$ 派でもさほど違和感はないだろうし、なによりコンフリクトが起きません。
プロファイルの書き方
圏の射のプロファイルは次のように書きます。
$`\quad f:A \to B \In\cat{C}`$
$`\cat{C}`$ が2-圏だとして、2-射のプロファイルは次のようです。
$`\quad \alpha :: f \twoto g : A \to B \In\cat{C}`$
$`\cat{C}`$ が3-圏だとして、3-射のプロファイルは次のようです。
$`\quad \Phi ::: \alpha \Rrightarrow \beta :: f \twoto g : A \to B \In\cat{C}`$
圏の対象は0-射です。0-射の宣言は次のように書きます。
$`\quad A \In\cat{C}`$
次のように、プロファイルの主要な部分だけ書いて残りは省略することもあります。
$`\quad A \In\cat{C}`$
$`\quad f:A \to B \In\cat{C}`$
$`\quad \alpha :: f \twoto g \In\cat{C}`$
$`\quad \Phi ::: \alpha \Rrightarrow \beta \In\cat{C}`$
出現するコロンの個数と矢印の“太さ”が射の次元と一致しています。スッキリしていて分かりやすいですね、僕のオススメの記法です。
型理論の記法
「GAT〈ガット〉の構文： スターリングの論文から」「実用になる型理論の記法」に書いたように、型理論の記法の特徴は：
- コロンとターンスタイル記号（'$`\vdash`$'）を矢鱈に（過剰に）使う。
なんでそこまでコロンとターンスタイルにこだわるのか？ 僕にはちょっと意味不明です。（他分野は考えないで）型理論のなかだけで考えても、コロンとターンスタイルのオーバーロードが激しいので、区別しにくい、理解しにくいという事態になります。型理論を圏論や論理と一緒に扱うときは、コロンとターンスタイルはただちにコンフリクトします。
僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合論の記法で書き換えてしまえばスッキリすると思うのですが ‥‥ コロンとターンスタイルの文化が型理論のアイデンティティの一部なんでしょうから、そうもいかないわけです。
型理論の記法の解釈の注意事項だけ述べておきます。
- 居住記号 '$`:`$' は集合論の所属記号 '$`\in`$' と解釈できることがある（できないこともある）。
- 居住記号 '$`:`$' は圏論のプロファイルコロンと解釈できることがある（できないこともある）。
- 居住記号 '$`:`$' は圏論のプロファイルにおける '$`\In`$' と解釈できることがある（できないこともある）。
- 判断ストローク '$`\vdash`$' は、圏論のプロファイル矢印と解釈できることがある（できないこともある）。
- 判断ストローク '$`\vdash`$' は、パイ型構成記号（後述）と解釈できることがある（できないこともある）。
- 判断ストローク '$`\vdash`$' は、演繹系の導出可能性記号と解釈できることがある（できないこともある）。
- 判断ストローク '$`\vdash`$' は、上位の演繹系のなかのオブジェクトレベル記号と解釈できることがある（できないこともある）。
コロンとターンスタイル（判断ストローク）を正しく解釈するには、型理論に対する演繹系を構成して、圏論的モデルを作って調べるしかないです。
パイ型構成
例えば、すべての集合に対する恒等写像達の族〈ファミリー〉 $`\id`$ は、次の集合に属すると考えられます。
$`\quad \id \in \prod_{X\in |\mbf{Set}|} \mrm{Map}(X, X)`$
ここで出てきた（大きな）集合がパイ型です。パイ型の書き方は色々あります。
- $`\prod_{X\in |\mbf{Set}|} \mrm{Map}(X, X)`$
- $`\prod(X\in |\mbf{Set}|).\, \mrm{Map}(X, X)`$
- $`\prod( X\in |\mbf{Set}| \mid \mrm{Map}(X, X) )`$
証明支援系では、パイ型を矢印で書くことがあります*2。
$`\quad (X : |\mbf{Set}|) \to \mrm{Map}(X, X)`$
これは手早く書けて便利なのですが、混乱が起きそうなので、僕は次の記法を使っています。
$`\quad [(X : |\mbf{Set}|) \dto \mrm{Map}(X, X)]`$
恒等写像達の族〈ファミリー〉はこの集合の要素なので：
$`\quad \id \in [(X : |\mbf{Set}|) \dto \mrm{Map}(X, X)]`$
これは、内部ホムを $`[A \to B]`$ と書く書き方とも整合性があります。
おわりに
現実の解釈（読解）では、まずグリフが目に入り、そのグリフがどんな意味を持つかを文脈から考えます。なので、グリフの多義性を知るのは解釈に役立ちます。が一方、先にグリフを考えるのではなくて、使用場面・使用意図を想定して、その文脈で使われる可能性のあるグリフを列挙してみることも、記号の多義性の整理には有効です。
