「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」において、矢印記号 '$`\to`$' やターンスタイル記号 '$`\vdash`$' のオーバーロードとコンフリクトが長年の悩みの種であることを述べました。
上記過去記事で次のように書きました。
エンテイルメント記号は、圏論のプロファイル矢印とコンフリクトしますが、これはしょうがないです。昔は、エンテイルメント記号に '$`\vdash`$' を使うことがありましたが、型理論との記号の奪い合いの抗争に疲れたので、今は使いません（'$`\vdash`$' は型理論に譲った）。
述語と部分集合の一対一対応を強調するときは、エンテイルメント記号に '$`\sqsubseteq`$' を使うこともあります。
「エンテイルメント記号に '$`\sqsubseteq`$'」 -- ん？ これいいかも！ 記号 '$`\sqsubseteq`$' のポピュラーな用法ってないよね。これをエンテイルメント記号にすれば、'$`\to`$' と '$`\vdash`$' のオーバーロード／コンフリクト問題は軽減しますね。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
%\newcommand{\dto}{\mathrel{!\!{\to}} }
%\newcommand{\dtimes}{\mathrel{!\!{\times}} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\id}{\mathrm{id} }
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\AS}{\mathop{ \mathrel{:\Leftarrow}} }
\newcommand{\Ent}{ \sqsubseteq }
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right]}
`$
内容：
シーケント
ゲンツェンの意味のシーケントは次の形です。
$`\quad A_1, \cdots, A_n \to B_1, \cdots, B_m`$
$`A_i, B_j`$ は論理式です。左辺と右辺の区切りに矢印 '$`\to`$' を使いましたが、'$`\Rightarrow`$' や '$`\vdash`$' を使うこともあります。いずれにしても記号のオーバーロード／コンフリクトの問題が発生します。ほんとに悩みの種なんですよ。
ここは思い切って、シーケントの区切り記号は '$`\sqsubseteq`$' に変更することにします。
$`\quad A_1, \cdots, A_n \Ent B_1, \cdots, B_m`$
左辺は右辺をエンテイル〈entail | 伴意 | ばんい | はんい〉すると読みます。
ついで(?)に、シーケントの書き方で不満だった点も変更してしまいましょう。
シーケントの左右は原則として丸括弧で囲むとします。ただし、丸括弧の省略は許容します。
$`\quad (A_1, \cdots, A_n) \Ent (B_1, \cdots, B_m)`$
カンマは、丸括弧内での区切り記号ですが、最後に余分なカンマがあるのは許容します。例えば：
$`\quad (A_1, \cdots, A_n,) \Ent (B_1, \cdots, B_m)`$
論理式がひとつもないときは $`()`$ ですが、カンマを残して $`(,)`$ でもかまいません。
$`\quad (,) \Ent (B_1, \cdots, B_m)`$
さて、ゲンツェン流のシーケントで嫌なところは、左辺のカンマと右辺のカンマの解釈が異なることです。右辺の区切り記号はカンマではなくて縦棒にします。
$`\quad (A_1, \cdots, A_n) \Ent (B_1\mid \cdots\mid B_m)`$
さきほど「カンマを残して $`(,)`$ でもかまいません。」と書きましたが、空リストには積極的に区切り記号を残します。例えば：
$`\quad (A_1, \cdots, A_n) \Ent (\mid )`$
左右ともに空リストなら：
$`\quad (,) \Ent (\mid )`$
シーケントの解釈の例
シーケントに対する簡単な解釈の事例を見ましょう。論理式には、たかだか1個の自由変数しか出てこないとして、便宜上（あくまで便宜上）変数名は $`x`$ とします。変数 $`x`$ が走る集合として $`X`$ を固定します。論理式 $`A`$ に対して、その意味を次のように決めます。
$`\quad \BR{A} := \{x\in X\mid A \}`$
この定義から：
- $`\BR{A} \subseteq X`$
- 同じことだが、 $`\BR{A} \in \mrm{Pow}(X)`$ （$`\mrm{Pow}`$ はベキ集合）
この解釈（意味付け）をもとに、シーケントの左辺、右辺、シーケント全体の意味を定めることができます。
$`\quad \BR{(A_1, \cdots, A_n)} := \BR{A_1}\cap \cdots \cap \BR{A_n}`$
$`\quad \BR{(B_1\mid \cdots\mid B_m)} := \BR{B_1}\cup \cdots \cup \BR{B_m}`$
$`\quad \BR{(A_1, \cdots, A_n) \Ent(B_1\mid \cdots\mid B_m) } := (\BR{(A_1, \cdots, A_n)} \subseteq \BR{(B_1\mid \cdots\mid B_m)})`$
要するに、シーケントの意味は集合の包含関係です。特に、空リストの場合は次のようです。
$`\quad \BR{(,)} := X`$
$`\quad \BR{(\mid)} := \emptyset`$
$`\quad \BR{(,) \Ent(\mid) } := (X \subseteq \emptyset)`$
シーケント $`(,) \Ent(\mid)`$ が意味的に“成立する”とは、集合に関する命題 $`X \subseteq \emptyset`$ が成立することなので、$`X = \emptyset`$ のことです。
前節で導入したシーケントの書き方と、この節の解釈ならば、記号の対応はけっこう自然です。
| シーケント | 集合 |
|---|---|
| $`,`$ | $`\cap`$ |
| $`\mid`$ | $`\cup`$ |
| $`\Ent`$ | $`\subseteq`$ |
さらには、シーケントの推論規則〈導出規則〉は、部分集合と包含関係に関する議論だと解釈できます。部分集合と包含関係は直感的でお馴染みでしょうから、シーケント計算が無理なく解釈できます。
圏におけるエンテイルメント関係
圏 $`\cat{C}`$ は2つのモノイド積を持つ圏だとします。このことを、記号の乱用により次のように略記します。
$`\quad \cat{C} = (\cat{C}, \otimes, \oplus)`$
なんらかの記号的表現（広義の論理式）に対して、圏 $`\cat{C}`$ の対象を割り当てる対応 $`\BR{\hyp}`$ があるとします。前節と同じようにして、カンマ区切りリストと縦棒区切りリストにも $`\BR{\hyp}`$ を拡張できます。
$`\quad \BR{(A_1, \cdots, A_n)} := \BR{A_1}\otimes \cdots \otimes \BR{A_n}`$
$`\quad \BR{(B_1\mid \cdots\mid B_m)} := \BR{B_1}\oplus \cdots \oplus \BR{B_m}`$
$`\quad \BR{(,)} := I`$
$`\quad \BR{(\mid)} := O`$
ここで、$`I`$ はモノイド積 $`\otimes`$ の単位対象、$`O`$ はモノイド積 $`\oplus`$ の単位対象です。
前節と違うことは、圏には包含関係がないことです。圏 $`\cat{C}`$ における包含関係 $`\subseteq_\cat{C}`$ を次のように定義します。
$`\text{For }X, Y \in |\cat{C}|\\
\quad (X \subseteq_\cat{C} Y) := (\cat{C}(X, Y) \ne \emptyset)
`$
'$`:=`$' の右辺は集合に関する命題ですから、普通に意味を持ちます。対象 $`X`$ から対象 $`Y`$ に向かう射が1本でもあれば、$`X \subseteq_\cat{C} Y`$ だとするのです。
ホムセット $`\cat{C}(X, Y)`$ の射（それがあれば）は、命題 $`X \subseteq_\cat{C} Y`$ の成立を保証する証拠〈witness〉となります。証拠を沿えた書き方は次のように約束します。
$`\quad X \subseteq_\cat{C} Y \text{ by }f`$
これは、次と同じことです。
- $`f\in \cat{C}(X, Y)`$
- $`f: X \to Y \In \cat{C}`$
今定義した $`\subseteq_\cat{C}`$ を使えば、シーケントの意味〈解釈〉を $`\cat{C}`$ において定義できます。
$`\quad \BR{(A_1, \cdots, A_n) \Ent(B_1, \cdots, B_m) } := \BR{(A_1, \cdots, A_n)} \subseteq_\cat{C} \BR{(B_1\mid \cdots\mid B_m)}`$
$`\quad \BR{(,)} := I`$
$`\quad \BR{(\mid)} := O`$
$`\quad \BR{(,) \Ent(\mid) } := (I \subseteq_\cat{C} O)`$
問題は軽減したが
シーケントの区切り記号、つまりエンテイルメント記号を '$`\Ent`$' に変更することにより、論理と圏論を一緒に議論するときの、矢印記号のオーバーロード／コンフリクトは解消されます。
ターンスタイルもシーケントの区切り記号には使ってないので、本来の用法、つまり導出可能性〈証明可能性〉として使えます。シーケントが、とある演繹系で導出可能なことは次のように書けます。
$`\quad \vdash (A_1, \cdots, A_n) \Ent (B_1\mid \cdots\mid B_m)`$
圏 $`\cat{C}`$ における解釈が決まっているなら、圏 $`\cat{C}`$ における妥当性は次のように書けます。
$`\quad \cat{C} \models (A_1, \cdots, A_n) \Ent (B_1\mid \cdots\mid B_m)`$
素晴らしい、平和が戻りました。
しかし、安心はできません。型理論ではターンスタイルが“導出可能性とは別な意味”で使われるでしょうから、型理論と一緒に議論するときは '$`\vdash`$' を導出可能性には使えません*1。
もし '$`\Ent`$' が他の意味で使われているなら、またしてもエンテイルメント記号を求めて放浪の旅に出る必要があります*2。
残念ながら、記号の奪い合いを根絶することはできません。
