論理では、矢印または矢印類似の記号がたくさん出てきます。それらの矢印記号に関連する名前や動詞もたくさんたくさんあります。記号と呼び名・動詞を表にまとめてみました。ただし、この表にはたいした根拠はありません。誰も根拠など持ってないと言っていいでしょう。
| 矢印記号 | 動詞 | 左側 | 右側 | 全体 |
|---|---|---|---|---|
| → | imply | antecedent | succedent | conditional proposition |
| ⇒ | derive | assumptions | conclusion | sequent |
| |- | prove | premises | statement | provability judgment |
| |= | satisfy | model | sentence | validity judgment |
| |⇒ | entail | facts | consiquence | semantic entailment |
世の中の標準がこの表だ、なんてことはまったくありません！ 僕がこんな言葉使いをしている、というわけでもありません。
論理における記号法／用語法は滅茶苦茶のグジャグジャです（論理に限ったことじゃないですが。例えば「型推論に関わる論理の概念と用語 その2」「絵算（ストリング図）における池袋駅問題の真相」参照）。似たりよったりの記号／言葉が山のようにあって、それらを明確に区別する人もいれば、同義語として使う人もいれば、なんだかワカラナイままに使っている人もいます。
この表は、先に枠組み（空欄の集まり）を作っておいて、そこに同じ言葉が入らないように埋めていったものです。出来るだけそれらしい言葉を選んだつもりではありますが。
類似の話題は次の記事でも扱っています。
いくつかの注意を述べておきます。
- 日本語を使うと、翻訳の曖昧性が入ってさらに話がややこしくなるので英語のままにしました。
- derive, prove, entail（名詞：derivation, proof, entailment）の区別は、あまりされてないと思います。僕もしてません。
- 含意記号（imply）は、→ 以外に ⊃ もよく使われます。僕は ⊃ を使うことが多いです。
- シーケント（sequent）の矢印は、→ も ⇒ も使われます。|- を使うこともあります。
- |- の右側をstatement、|= の右側をsentenceとしたのは苦し紛れです。conclusionかconsiquenceを使うことが多いと思います。
- satisfy, model, sentenceはインスティチューションの用語です。インスティチューションでは、|= をsatisfaction relationと呼びます。
- 動詞として、deduce, refine, infer, reasonなどもありますが、この表では使ってません。
- |- を使ったjudgmentの左（premisesと書いた）はcontextということもあります。特に型理論ではcontextが多いです。
記号法／用語法だけでなく、内容的な補足をちょっとしておきます。
|-, |=, |⇒ は論理システム（演繹系、論理の形式的体系）の内部で使う記号ではなくて、メタな言明を記述するために使います。ただし、|- はシーケントの区切りにもよく使われているので、そのときはシーケント計算（という論理システム）の内部の記号です。
Sをなんらかの論理システムだとして、AをSの論理式（formula）、ΦをSの論理式の集合だとします。このとき、Φ |-S A は、Φに含まれる論理式を仮定した場合にAを証明できることを表します。Sが事前に分かっているなら、下付きのSは省略します。Φが有限集合 {B1, ..., Bn} ならば、B1, ..., Bn |- A と書きます。特に、Φが空集合なら |- A ですね。
|- は構文論的（証明論的）な概念を表しますが、|= は意味論的（モデル論的）概念を表します。Mがモデルのとき、M |=S A は、論理式AがモデルMに対して成立することを表します。|=S をキチンと定義するのはそれほど楽じゃありません。
モデルの集合をU（宇宙）として、Uに所属する任意のモデルMに対して M |=S A であるとき、|=S A と書きます。Sが了解されているなら |= A です。ほんとはUも明示したほうがいいのでしょうが、暗黙に決まっているとして省略します。
論理システムS、意味論的妥当性 |=S、宇宙Uが決まっている状況で、Φ |⇒ A は次のような意味です。
- B∈Φ である任意の論理式Bに対して M |= B であるなら、必ず M |= A である。
Φ |- A と Φ |⇒ A は似てますが、Φ |- A は構文論的な主張で Φ |⇒ A は意味論的な主張です。
「論理における記号法／用語法は滅茶苦茶のグジャグジャ」と言いましたが、論理と関連したソフトウェアである証明支援系では、さらに輪をかけて酷いことになります。論理の用語に加えてアルゴリズムや実装に由来する用語が入り、コミュニティの隠語も混ざってきます。例えば、Coqにおける「ゴール」という言葉の困った使い方。
証明支援系はカリー／ハワード対応を使うことが多いので、型理論の用語も使います。型理論の用語法はいいかげん混乱してますが、この混乱も持ち込まれます。
その結果、証明支援系のマニュアルや解説の記述は悲惨なことになります。冒頭の一覧表（の枠組み）を作った動機は、Isabelleのマニュアルの激しく曖昧・多義的な用語法を整理するためでした。
論理や論理的ソフトウェアが自分自身を語るときの論理性や整合性がグダグダなのは、「なんとかならんのかよ」と思います。
