「論理／メタ論理の記法をどうするか」の続き。書き方（構文、記法）の話です。いきなり「どう書こうが同じだろ」「書き方なんて何だっていいじゃねーか」と言って済ますことが出来るなら楽なんだけど … そうもいかないのですよねー。
悩みと迷いとウンザリを繰り返せば、いずれは「どう書こうが同じだろ」「書き方なんて何だっていいじゃねーか」の境地＝悟りに到れるかも。
内容：
含意記号について
最近は、含意記号に二本棒矢印'⇒'を使うことが多いです。しかし、もともと僕は、'⇒'を使う習慣はなくて、'⊃'を使っていました。'⇒'も使うようになった理由は、'⊃'を知らない人が多くて違和感を持たれてしまうからです。
2006年の記事「論理記号のいろいろ」で引用した次の表を見てみると：
含意に'⇒'を使っている例ってないんですよね。僕がよく使っていた記法は、「竹内 1975」と同じです（竹内外史さんは、含意に'→'も使っています）。次の記事内（節の冒頭）では、使う記号を確認したりしています。
僕の本音としては、含意に'⇒'を使いたくない。二本棒矢印は、別な目的で使いたいのです。一本棒矢印も含意以外で使いたいこと多いし。論理ではいろいろな矢印が出てくるので、矢印記号が不足して困るんですよ。次の記事参照。
ところで、いま僕は「含意記号」といいましたが、「ならば」を意味する記号は条件記号〈conditional symbol〉と呼び含意記号〈implication symbol〉とは呼ばない人もいます*1 -- 含意〈implication〉と条件法〈conditional〉を別な意味で使うのです。条件法とは区別された含意を《含意》と書くことにして、「命題Aが命題Bを《含意する》」とは、
- 条件命題 A⊃B が成立すること。
「へっ？」という感じもしますが、条件記号'⊃'は、単なる論理結合子〈論理演算子〉であって、《含意する》はメタ論理の概念なんです。
《含意》を上記のように解釈するとして、ある演繹システムSによる証明可能性を |-S と書くと、次の3つのメタ命題は同値です。
- Sにおいて、AがBを《含意する》。
- |-S A⊃B （Sにおいて、仮定なしに、条件命題 A⊃B を証明できる。）
- A |-S B （Sにおいて、命題Aを仮定して、命題Bを証明できる。）
これは《含意》の構文的解釈（証明論的解釈）ですが、意味的解釈（モデル論的解釈）もできます。
たぶん、含意記号／含意命題と条件記号／条件命題を別物として扱う人は少数派だと思うので、僕は「含意」と「条件／条件法」を区別してません。上記のようなメタ論理的な概念が必要なら、メタ論理記号である '|-'（証明可能）、'|='（妥当）、'|⇒'（伴意）などを使ってその旨を表現します（前回記事も参照）。
変数宣言と仮定
定理・公理の記述として、変数（自由変数）の宣言の前には'For'、仮定の命題の前には'Given'、結論の命題の前には'Holds'を付けた書き方をしてみます。
For x∈R For y∈R Given x≧0 Given y≧0 Holds x + y ≧ 0
こういう丁寧な書き方をしていた時期もあったのですが、めんどくさくなって、変数宣言も仮定も一律に'For'（または一律に'Given'）になってしまいました。さらには、キーワード書くのもめんどうなんで、結局は次のような形：
- x∈R, y∈R, x≧0, y≧0 → x + y ≧ 0
これって結局、シーケント〈sequent〉の構文です。シーケントを知らない人は、今言った形がシーケントだと思えばいいです。つまり、矢印'→'の左側に変数宣言と仮定命題を書いて、右側に結論命題を書いた形です。
シーケントの左右区切りとして出てくる矢印と、含意記号を区別する必要があるので、含意に'⇒'を使いたくなかったのです。記号の使い方の案は：
| 含意記号 | シーケントの左右区切り記号 | |
|---|---|---|
| 案1 | ⊃ | ⇒ |
| 案2 | → | ⇒ |
| 案3 | ⊃ | → |
| 案4 | ⇒ | → |
案1と案2は竹内外史さんが使っていた記法です。案3は、'⇒'を別な目的で温存したいときに僕は使っています。案4は含意に'⇒'を使ってしまったときの用法です。ここではとりあえず、案3を使います。
シーケントの左右区切りに'|-'を使うこともけっこうあります。ですが、形式的シーケント計算内で'|-'を使うのはどうかな？ という気もします。なぜなら、'|-'はメタ論理の「証明可能性」で使う記号ですから。形式的体系（人工的な記号操作のメカニズム）としてのシーケント計算のシーケントは、メタ論理的な意味も捨象されています。もちろん、“証明可能性の計算”をするときなら、シーケントの左右区切りに'|-'を使うのは適切です。
シーケントの左側には変数宣言と仮定の命題が並びます。変数宣言と仮定の命題の違いは見ればわかりますが、念の為、変数宣言は丸括弧で囲むことにします。
- (x∈R), (y∈R), x≧0, y≧0 → x + y ≧ 0
複数の変数宣言を、まとめて丸括弧内に入れてもいいとします。
- (x, y∈R), x≧0, y≧0 → x + y ≧ 0
定理・公理記述の変形とシーケント計算
以前に述べた証明のお膳立ての操作は、形式化すればシーケント計算に吸収されるでしょう。言い方を換えれば、シーケント計算（シーケントの変形）は、日常的に知らず知らずに使っているのです。
重要かつ典型的なシーケントの変形に次があります。
Γ, A → B -------------↓↑ Γ → A⊃B Γ, (x∈X) → A -----------------↓↑ Γ → ∀x.A
ここで、Γ（大文字ガンマ）はその他諸々の変数宣言／仮定命題です。「↓↑」が付いているのは、上下両方向の変形が許されるからです。シーケントの矢印'→'は、証明可能性判断〈provability judgement〉の'|-'だと思っても、証明要求〈proof requirement〉の'|-?'だと思っても、どっちでも通用します。証明要求については、次の記事を参照：
シーケントの'→'を意味的帰結〈semantic consequence | entailment〉と解釈すれば、シーケント計算は、（形式化された）“事実の記述”の計算になります。意味的帰結については前回記事参照：
定理・証明の変形の書き方
この記事のタイトルは「記法をどうするか」です。内容にはあまり踏み込まず、記法（書き方）だけを問題にします。
前節の Γ, A → B などは、ひとつの定理の前提と結論の記述だとみなします。そして、矢印の部分に証明が詰め込まれていると考えましょう。詰め込まれている感じを出すために、Γ, A |→| B のように書き方を変えます。記号 '|→|' は、「この部分に証明が入る」という意味だと捉えてください -- ただし、あくまで気分だけの話です。
次に、「横の物を縦にする*2」ことにします。
Γ, A ------ ↓ ---- B
見栄えをよくするために、横棒（'-'の並び）の長さを変えてますが、これは必須ではありません。'-'は4個とかに固定してもいいです。
前節の「変形する」の意味の横棒は、二重線（'='の並び）に切り替えます。すると、前節と同じ絵図が次のように変わります。
Γ, A
----
↓
----
B
=========↓↑
Γ
----
↓
----
A⊃B
Γ, (x∈X)
----
↓
----
A
=========↓↑
Γ
----
↓
----
∀x∈X.A縦にスペースを取りすぎる気もします。二重線を縦棒にして左右に並べてみましょうか。
Γ, A ‖ Γ
---- ‖ ----
↓ ‖ ↓
---- ‖ ----
B ‖ A⊃B
←→
Γ, (x∈X) ‖ Γ
---- ‖ ----
↓ ‖ ↓
---- ‖ ----
A ‖ ∀x∈X.A
←→
二重線の縦棒を並べるのはけっこうな手間だし、レイアウトが崩れてガタガタになったりするので、縦棒を横矢印にしてみます。
Γ, A Γ
---- ----
↓ ⇔ ↓
---- ----
B A⊃B
Γ, (x∈X) Γ
---- ----
↓ ⇔ ↓
---- ----
A ∀x∈X.A
以上のような描き方（図の記法）の変更をしても、内容的には何も変わってません。ですが、描画方向や使っている印が違っただけで、「難しい」「分からない」となってしまうことが多いのです。これは残念なことです。
縦の物を横にする、横の物を縦にする、印を置き換える、といった操作を躊躇なく自由に出来る能力はほんとに重要です。以下の記事は、圏論のストリング図の話として書いてますが、論理の横棒記法の図でも事情は同じです。図の描き換えの練習をしましょう。
リーズニングの図示
今は、シーケントの矢印に'→'を使っています。場合により、'→'が、'⇒', '|-', '|-?', '|⇒' なんかに変わるかも知れません。これらの区切り記号をシーケント区切り記号〈sequent delimiter〉と呼ぶことにします。シーケント区切り記号の変化に過敏に反応したり、惑わされないようにしましょう。
シーケントを変形する操作をリーズニング〈reasoning〉と呼びましょう*3。リーズニングを表す記号はリーズニング記号〈reasoning symbol〉ということにします。
リーズニングを図示する際には、次の選択をすることになります。
- シーケント区切り記号は、どれを使うか？
- シーケントの方向を、どの方向にするか？
- リーズニング記号は、どれを使うか？
- リーズニングの方向を、どの方向にするか？
幾つかの例を挙げてみます。
- シーケント区切り記号： |→|
- シーケントの方向： 左から右（→）
- リーズニング記号： '='の並び
- リーズニングの方向： 上から下（↓）
Γ, A |→| B ===============↓ Γ |→| A⊃B
- シーケント区切り記号： 縦に書いた |→|
- シーケントの方向： 上から下（↓）
- リーズニング記号： '='の並び
- リーズニングの方向： 上から下（↓）
Γ A ---- ↓ ---- B ======↓ Γ ---- ↓ ---- A⊃B
- シーケント区切り記号： →
- シーケントの方向： 左から右（→）
- リーズニング記号： ⇒
- リーズニングの方向： 左から右（→）
Γ, A → B ⇒ Γ → A⊃B
- シーケント区切り記号： ':'の縦並び
- シーケントの方向： 上から下（↓）
- リーズニング記号： ⇒
- リーズニングの方向： 左から右（→）
Γ A Γ : : : ⇒ : : : B A⊃B
横書きテキストだと、変数宣言や命題を並べる方向は左から右に限定されますが、絵（イラスト、ピクチャ）なら、その方向も自由になります。A, B, C → D というシーケントは次のように書くかもしれません。
A B → D C
他に：
- 変数宣言や命題に名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。
- シーケントに名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。
- リーズニングに名前〈ラベル〉を付けるかも知れない。名前の付け方や付ける場所の選択肢・自由度がある。
要するに、書き方・描き方には、ものすごいバリエーションがあるってことです。しかし、中身・内容は何も変わらない、一緒なんです。書き方・描き方のバリエーションに対応するには、自分でいろいろな書き方・描き方を試してみるのが一番です。
リーズニングのテキスト表現
最後に、リーズニングを横書きテキストだけで書き表すときの書き方について考えます。各種の矢印記号をどう選ぶか？ がポイントです。含意記号の選び方が、シーケント区切り記号とリーズニング記号の選び方に影響します。
| 含意記号 | シーケント区切り記号 | リーズニング記号 | |
|---|---|---|---|
| 案1 | ⊃ | → | ⇒ |
| 案2 | → | ⇒ | ▷ |
| 案3 | ⇒ | → | ▷ |
リーズニングに三角を選んだのは僕の恣意的選択です（これといって根拠などない）。
次のリーズニングを例題にしましょう。
before For x∈R For y∈R Given x≧0 Given y≧0 Holds x + y ≧ 0 after For x∈R For y∈R Given x≧0 Holds y≧0 ならば x + y ≧ 0
案1を使うと：
- (x∈R), (y∈R), x≧0, y≧ → x + y ≧ 0 ⇒ (x∈R), (y∈R), x≧0 → y≧0 ⊃ x + y ≧ 0
案2を使うと：
- (x∈R), (y∈R), x≧0, y≧ ⇒ x + y ≧ 0 ▷ (x∈R), (y∈R), x≧0 ⇒ y≧0 → x + y ≧ 0
案3を使うと：
- (x∈R), (y∈R), x≧0, y≧ → x + y ≧ 0 ▷ (x∈R), (y∈R), x≧0 → y≧0 ⇒ x + y ≧ 0
どうでしょう？ 「ややこしいな」「紛らわしいな」と思いましたか？ その通りです。もし、「結局、どう書いても一緒じゃん」と思えたなら、それは「悟り」です。悟りは「拘り」を捨てることであり、「諦め」と似ています。諦めは「呆れた」とほぼ同じです。「もう呆れたよ、諦めたよ、拘ってもしょうがないね」 -- と、そう悟ってください。
