昨日の記事「エンテイルメント記号とシーケント」において、従来のシーケントの書き方は変更したほうがいいと提案しました。この機会に、シーケントに対する長年の不満とその対策を記しておきます。$`
\newcommand{\Imp}{\Rightarrow }
\newcommand{\Ent}{ \sqsubseteq }
`$
内容：
シーケントの書き方
昨日の記事「エンテイルメント記号とシーケント」の要点は、シーケントを次のように書こう、ということです。
- 左辺と右辺を区切る記号（エンテイルメント記号）に '$`\Ent`$' を使う。
- 論理式のリストを囲む丸括弧を省略しない。
- リスト内で論理式を区切る区切り記号を左辺と右辺では変える。具体的にはカンマと縦棒。
- 空リストには区切り記号（カンマか縦棒）を残す。
論理だけを語る文脈では、エンテイルメント記号に '$`\to`$' を使っても何の問題もありません。が、圏論や型理論も一緒に語る文脈ではコンフリクトや誤認が生じます。
- 矢印記号 '$`\to`$' は、圏論のプロファイル矢印とコンフリクトする。
- 二重矢印記号 '$`\Imp`$' は、含意記号とコンフリクトする。含意に別な記号（例えば '$`\supset`$'）を使ったにしても、二重矢印を含意記号と誤認する人がいる。
- ターンスタイル記号 '$`\vdash`$' は、演繹系の導出可能性〈証明可能性〉を表すメタ記号とコンフリクトする。型理論の判断ストロークともコンフリクトする。
「オーバーロードやコンフリクトは日常茶飯事なのだから、そんなに気にすることないよ」と思う人もいるでしょう。僕もかつてはさほど気にしてませんでした。が、ここ10年くらいの経験で、「オーバーロード／コンフリクトを適切に処理する」ことは、とてもとてもとても難しいことだ、と痛感しました。オーバーロード／コンフリクトを完全に避けるのはどうせ無理なのは重々承知ですが、できるだけ避ける努力はするべきだと思っています。
ある程度慣れれば、エンテイルメント記号にどんな記号を使おうがどうでもいいと達観できますが、入口では、オーバーロード／コンフリクトが大きな障害になります。
リストの囲み記号、リスト内の区切り記号がなぜ問題になるかの背景は次節以降で説明します。
コンパクトシーケント
ゲンツェンのオリジナルのシーケントの（もちろんバリエーションはありますが）比較的標準的な書き方は以下です。
$`\quad A_1, \cdots, A_n \to B_1, \cdots, B_m`$
僕が望ましいと思う書き方は以下です。
$`\quad (A_1, \cdots, A_n) \Ent (B_1\mid \cdots\mid B_m)`$
特に、両辺が空の場合は差が出ます
- $`\to`$ （左右に何も書かない）
- $`(,)\Ent (\mid)`$
区切り記号をカンマと縦棒のニ種類使うのは、解釈が異なるからです。
コンパクトシーケント〈compact sequent〉とは、左右の区切り記号の解釈が同じシーケントのことです。ゲンツェンのシーケントの区切り記号をカンマだけで書くと、コンパクトシーケントとの区別ができません。カンマと縦棒を使うなら次のように区別できます。
- ゲンツェンのシーケント： $`(A_1, \cdots, A_n) \Ent (B_1\mid \cdots\mid B_m)`$
- コンパクトシーケント： $`(A_1, \cdots, A_n) \Ent (B_1, \cdots, B_m)`$
圏論的解釈のとき、ゲンツェンのシーケントは2つのモノイド積を持つ圏でないと解釈できません。それに対して、コンパクトシーケントは通常のモノイド圏で解釈できます。
区切り記号（カンマと縦棒）をモノイド積で解釈する以外に、コンパクトシーケントを多圏〈polycategory〉で解釈することもできます（「述語論理： 様々な多圏達の分類整理」参照）。ゲンツェンのシーケントは多圏では解釈できません。
ゲンツェンのシーケントにおける両辺とも空なシーケント $`(,)\Ent (\mid)`$ は矛盾を表すので、証明〈導出〉されては困るシーケントです。しかし、コンパクトシーケントにおける両辺とも空なシーケント $`(,)\Ent (,)`$ は常に導出可能〈証明可能〉な当たり前のシーケントです。矛盾と当たり前の区別が出来ないのはほんとに困ります。
このような事情で、区切り記号はニ種類使い、リストの囲み括弧も省略しないのが良いと思うのです。
右単元シーケントと左単元シーケント
「単元」は"singleton"の翻訳語として使います。右単元シーケント〈right singleton sequent〉は次の形のシーケントです。
$`\quad (A_1, \cdots, A_n) \Ent B`$
左辺がリストではなくて単一の論理式（一般にはなんらかの項）です。
コンパクトシーケントが多圏で解釈できるのと同様に、右単元シーケントは複圏〈オペラッド〉で解釈できます。左辺リストは複圏の対象のリスト、右辺は複圏の対象、シーケント全体は複射と解釈します。
左単元シーケント〈left singleton sequent〉は次の形です。
$`\quad A \Ent (B_1, \cdots, B_n)`$
左単元シーケントは、余複圏（複圏の双対概念）で解釈できます。左辺は余複圏の対象、右辺リストは余複圏の対象のリスト、シーケント全体は余複射ですね。
前節で出した多圏、この節で出した複圏／余複圏は、モノイド圏から構成することが多いですが、必ずしもモノイド圏由来である必要はありません。
右片側シーケントと左片側シーケント
片側シーケントは、左辺または右辺が空リストであるシーケントです。空リストの解釈により意味が変わってきます。空リストとして $`(,)`$ と $`(\mid)`$ を区別します。
リストの区切り記号の選び方により、次のような片側シーケントがあり得ます。
- $`\quad (,) \Ent (B_1, \cdots, B_m)`$
- $`\quad (,) \Ent (B_1\mid \cdots\mid B_m)`$
- $`\quad (\mid) \Ent (B_1, \cdots, B_m)`$
- $`\quad (\mid) \Ent (B_1\mid \cdots\mid B_m)`$
- $`\quad (A_1,\cdots, A_n) \Ent (,)`$
- $`\quad (A_1\mid \cdots\mid A_n) \Ent (,)`$
- $`\quad (A_1,\cdots, A_n) \Ent (\mid)`$
- $`\quad (A_1\mid \cdots \mid A_n) \Ent (\mid )`$
これらは、ゲンツェンのシーケント、またはコンパクトシーケントの特別な場合と解釈できます。
注意しないといけない点は、例えば $`(,) \Ent (B_1, \cdots, B_m)`$ を $`(B_1, \cdots, B_m)`$ と略記したり、$`(A_1,\cdots, A_n) \Ent (\mid)`$ を $`\quad (A_1,\cdots, A_n)`$ と略記することがあることです。片側しかないので、空である側は省略しても情報は変わりませんが、解釈がまったく違ってしまうことがあります。片側であっても省略しないで書くことをオススメします。
名前付きと名前無し
シーケントには幾つかの論理式（一般にはなんらかの項）が出現しますが、論理式に名前を付けることがあります。名前と論理式はコロンで区切ることが多いです。例えば、次のように：
$`\quad (\alpha_1 : A_1, \cdots, \alpha_n: A_n) \Ent \beta : B`$
「型理論のコロン、ターンスタイル、カンマ」で述べたように、型理論ではコロンが使われすぎなので、使わなくて済むところではコロンを使わないようにしたいですね。
コロンの代わりに所属記号を使うと、違和感をいだく人が多いでしょう。
$`\quad (\alpha_1 \in A_1, \cdots, \alpha_n \in A_n) \Ent \beta \in B`$
実際には、論理式の意味も集合だと解釈することが多いので、別に問題はありません。問題は、「なんか気持ち悪い」という人の感情のほうです。
人の感情をまったく無視もできないので、コロンと所属記号の折衷案で次のように書いてもいいでしょう。
$`\quad (\alpha_1 \in: A_1, \cdots, \alpha_n \in: A_n) \Ent \beta \in: B`$
$`\in:`$ の圏論的な解釈は、デフォルトの対象（多くの場合は終対象） $`X`$ に対する $`X\to`$ の略記です。つまり、省略しないで書くと：
$`\quad (\alpha_1 : X \to A_1, \cdots, \alpha_n : X \to A_n) \Ent \beta : X \to B`$
名前が付いてないときの解釈は二通りあります。
- ほんとは名前が付いているのだが省略している。
- 名前など最初から考えてない。
どちらであるかは、文脈から判断するしかないですね。「名前を使うなら絶対に省略するな」というルールは、厳しすぎて守れないでしょう。
シーケントと判断
論理で使うシーケントと、型理論で使う判断〈judgement〉はどんな関係があるのでしょうか？ Propositions-as-Types の立場をとるならば、論理式は型項とみなせます。シーケントは判断とみなせます。
ただし、判断はシーケントより詳細な情報を記述しているので、シーケント側でも追加の情報が必要です。追加情報付きのシーケントとして、次の形を考えます。
$`\quad (\alpha_1 \in: A_1, \cdots, \alpha_n \in: A_n) \Ent B \text{ by }t`$
ここで、$`t`$ は導出ツリー〈証明ツリー | 証明項〉です。導出ツリーを考えるということは、なんらかの演繹系（「演繹系とオペラッド」参照）を前提しているということです。導出ツリーを伴ったシーケントは、論理式達のあいだの関係を記述しているだけでなくて、その根拠・証拠も一緒に持っています。ただし、その根拠・証拠が正しいかどうかは別問題です（検証を要する）。
上記の導出ツリー付きシーケントの別な書き方が次です。
$`\quad (\alpha_1 \in: A_1, \cdots, \alpha_n \in: A_n) \vdash t \in: B`$
$`t`$ は導出ツリー〈証明項〉なので、単なる名前とは限りません。
導出可能性
型理論は、ターンスタイル記号を区切り記号とする判断を文〈構文的対象物〉とする演繹系を持っています。演繹系の内部の記号（オブジェクトレベルの記号）としてターンスタイル '$`\vdash`$' を使っているので、導出可能性を表すメタ記号は '$`\Vvdash`$' とします。'$`\Vdash`$' は整形式性〈well-formedness〉を表すメタ記号として取っておきます（今日は使いません）。
論理だけの話でも、論理と型理論を混ぜた話でも、演繹系が複数登場します。つまり、「導出可能」だと言っても、どの演繹系により導出可能かが問題になります。一律に '$`\Vvdash`$' だけだと区別がつきません。演繹系 $`D`$ による導出可能性は '$`\Vvdash^D`$ と書くことにします。上付きにしているのは、下付きを別な目的で使うからです。
$`ND`$ が自然演繹スタイルの演繹系、$`SC`$ がシーケント計算スタイルの演繹系、$`TT`$ が型理論スタイルの演繹系とすると、同じことを演繹系ごとに違う形で表現することになります。
まず、有名な演繹定理は次の2つが同じことだと主張しています。
- $`A \Vvdash^{ND} B`$
- $`\Vvdash^{ND} A\Imp B`$
記号 '$`\Vvdash^{ND}`$' の左側は、仮定する（公理扱いする）論理式です。左側に何もないことは、何も仮定しないことです。「何も仮定しない」ことと「真（$`\top`$）」を仮定するのは同じですから、以下の2つは同じことです。
- $`\Vvdash^{ND} A`$
- $`\top \Vvdash^{ND} A`$
自然演繹スタイルとシーケント計算スタイルでは、次の2つが同値になるように演繹系を設計するのが普通です。
- $`A_1, \cdots, A_n \Vvdash^{ND} B`$
- $`\Vvdash^{SC} (A_1, \cdots, A_n) \Ent B`$
特に、次の2つは同値になるようにします。
- $`\Vvdash^{ND} B`$
- $`\Vvdash^{SC} (,) \Ent B`$
シーケント計算スタイルと型理論スタイルでは、次の2つが同値になるように演繹系を設計するのが普通です。
- $`\Vvdash^{SC} (\alpha_1 \in: A_1, \cdots, \alpha_n \in: A_n) \Ent B\text{ by }t`$
- $`\Vvdash^{TT} (\alpha_1 \in: A_1, \cdots, \alpha_n \in: A_n) \vdash t \in: B`$
この場合、ツリー〈項〉 $`t`$ を書き下すために名前達 $`\alpha_1, \cdots, \alpha_n`$ が必要です。
オブジェクトレベル（演繹系の内部）の記号とメタレベルの記号を区別するだけでなく、色々な演繹系による導出可能性〈証明可能性〉も区別しないと、メタレベルの議論は意味不明となってしまいます。
おわりに
いつも言っていることですが、「構文側／意味側、オブジェクトレベル／メタレベル、地の文／形式表現、提示／主張 などの区別が出来る人にとっては、オーバーロード／コンフリクトの回避など不要」です。むしろ、色々な記号や言い方を使い分けるのは煩雑であり邪魔でしょう。
しかしだからと言って、オーバーロード／コンフリクトの回避策が誰にとっても不要で邪魔くさい、とはなりません。少なくとも導入段階では、オーバーロード／コンフリクトの回避策を講じないと、混同・混乱してしまうケースが多いです。「過剰なオーバーロード／コンフリクトは人を苦しめる」というのが、今の僕の見解です。
