矢印記号の使い方が、分野やコミュニティごとにバランバランで困ったー、という話題は、大昔から何度も繰り返しています。
- さまざまな「ならば」達 (2006年)
- 論理記号のいろいろ (2006年)
- 論理：証明可能性と普遍妥当性 (2009年)
- 型推論に関わる論理の概念と用語 その1 (2012年)
- 論理におけるさまざまな「矢印」達 (2016年)
- 論理／メタ論理の記法をどうするか (2018年)
- 論理／メタ論理の記法をどうするか 2: 悟りへの道 (2018年)
- 互換な演繹システムとシーケント、そして矢印記号 (2020年)
- コンテキスト、判断、指標、シーケントなどのゴチャゴチャを整理 (2022年)
- 矢印の混乱に対処する： デカルト閉圏のための記法 (2023年)
- 矢印のオーバーロードがひどい件： 所感 (2023年)
2024年5月末時点では、次が良かろうと思っています。主に型理論で使う場合を想定していますが、論理でも出来るだけ同じ記号を使いたいですね。
| 矢印記号 | 読み方 | 左側 | 右側 |
|---|---|---|---|
| $`\Rightarrow`$ | 含意〈implies〉 | 前件 | 後件 |
| $`\vdash`$ | 伴意〈entails〉 | コンテキスト | |
| $`\rightrightarrows`$ | 推論〈infers〉 | 前提 | 結論 |
| $`\Vdash`$ | 正当〈correct〉 | (なし) | コンテキスト |
| $`\Vvdash`$ | 導出可能〈derivable〉 | システム | 判断 |
| $`\models`$ | 充足〈satisfies〉 | モデル | 文 |
含意
'$`\Rightarrow`$' は論理結合子〈logical connective〉記号です。演算記号であって、関係記号ではありません。含意演算の記号には '$`\supset`$' を使うこともあります。昔、僕は '$`\supset`$' だけを使っていたのですが（シーケントの区切り記号に '$`\Rightarrow`$' を使っていたので）、最近は含意に二重矢印記号 '$`\Rightarrow`$' を使うことが多くなりました。
伴意
型理論において、判断〈judgement〉の左辺と右辺を区切る記号です。伴意記号 '$`\vdash`$' の左辺はコンテキストで、右辺は色々です。この記号自体はターンスタイルと呼びます（「ターンスタイルって知っている？」参照）。
論理のシーケントの区切り記号にも '$`\vdash`$' を使ってもいいと僕は思いますが、証明可能〈provable〉のメタ記号が '$`\vdash`$' なので、それが問題になるかも。
推論
推論図は通常、横棒で上段と下段に区切って書きますが、そのときの横棒を左右方向に書いた場合の矢印が '$`\rightrightarrows`$' です。モーダスポネンスの推論図なら次のようです。
$`\quad A \quad A\Rightarrow B \;\rightrightarrows\; B`$
次は、形の上では論理AND〈連言〉の導入規則に見えます。
$`\quad \Gamma \vdash A \quad \Gamma \vdash B \;\rightrightarrows\; \Gamma \vdash A\land B`$
型理論では、項の形成規則〈formation rule〉になります。文法なら構文生成規則〈production rule〉です。構文的に許される形式であることと、それが証明されたことは別なことですが、区別しにくいときはあります。
正当
'$`\Vdash`$' は、コンテキストが構文的に正当なことを表現するために、次のように使います。
$`\quad \Vdash \Gamma`$
通常のターンスタイルを使って、右側に何も書かない流儀が多数派です。
$`\quad \Gamma \vdash`$
これは視認性が良くないし、解釈にも悩むので別な記号 '$`\Vdash`$' を使ったほうがいいと思います。
構文的に正当なことは、整形式〈well-formed〉とか正統〈legitimate〉とか合法〈legal〉とか妥当〈valid〉ともいいます。が、「妥当」は意味論的な妥当性にだけ使ったほうが無難でしょう。
導出可能
型理論的システム〈type-theoretic{cal}? system〉 $`S`$ において、判断 $`\Gamma \vdash A`$ が導出可能なことを次のように書きます。
$`\quad S \Vvdash \Gamma \vdash A`$
型付け判断〈typing judgement〉 $`\Gamma \vdash t:A`$ が導出可能なら次のように書きます。
$`\quad S \Vvdash \Gamma \vdash t:A`$
これを、PAT-PAT〈propositions as types, proofs as terms〉解釈するなら、命題 $`A`$ の証明項〈proof term〉 $`t`$ が構成可能であることになります。つまり、システム〈形式的体系〉 $`S`$ 内で $`A`$ は証明可能〈provable〉です。
その他
シンプルな矢印 '$`\to`$' は圏論で多用するので、ここでは使わないことにしています。とはいえ、'$`\Rightarrow`$' だって2-射を表すのに使うので、どうしたってコンフリクトは起きます。
演繹〈deduction | deduce〉という言葉は、複数の証明をひとまとめにしたモノという意味で使いたいと思っています。例えば、ある公理系を別な公理系でシミュレートするときの証明の集まりは演繹です。演繹を表す矢印は？ ウーン、一周回ってシンプルな矢印 $`\Delta \to \Gamma`$ とか、コンテキスト射の一種ですから。
意味論的帰結〈semantic consequence〉であることは、また別な矢印 '$`|\!\!\Rightarrow`$' とかで表すしかないでしょうね。'$`\models`$' を流用すると誤解をまねきそうですから。
形式的体系（の一部）は項書換え系であることが多いですが、書き換えの矢印は '$`\leadsto`$' とか '$`\mapsto`$' ですかね。
