0. 概要

数学では「ならば」に相当するような記号や表記や概念がたくさん出てくるので整理してみた。数理論理学に関連。

1. 「ならば」っぽい奴の一覧

→, ⊃
- 論理学の「ならば」。真理値表を書けばその機能は明確。A→Bのように使われAがtrueかつBがfalseの時にのみfalseとなる。定義が明確なので使用上の混乱はないが、「なぜその真理値表を持つのか？」というそもそもの疑問を持つ人もいる（→をならばと読んでいるからこその疑問）
定理における ⇒, $\Longrightarrow$, ならば
- 定理の中に出てくる日本語「ならば」。⇒や $\Longrightarrow$ とも。
- 例「xが4の倍数ならば xは2の倍数である」
- 「AならばB」という形で文の間に配置されて、新しい言明を生成する。Aが成立していないときのことについては何も主張しないのでその時の B の成否は問わない。
- メタな文（論理式で表せない文）とメタな文の間に配置して、新しい言明を生成することもある
- 人によっては頭の中で自動的に A→B に翻訳しているかもしれない（がそれは先走りすぎかも。後述。）
ならば（日常）
- 日本語などの自然言語での「ならば」。「雨が降るならば遠足は中止です」に見られるように、雨が降らない場合も暗示することもある（つまり、雨が降らなかった時には遠足は行うといったように。この場合、ならばというよりも同値となる）。数学のテクストも日本語で記載されるので、自然言語での説明や解説において影響がありうる。
⊢, 「・・を仮定するならば・・が証明できる/導出できる」
- 「AとBを仮定するならばCが導出できる」のように使われる。論理学では ⊢ という記号を用い、{A,B} ⊢ C と書く。
- 公理と定理の関係もこのカテゴリに入る。
- 上述の「⇒」と似ているがこちらの方が意味が限定されている。「⇒」の証明ヴァージョンが「 ⊢ 」だと理解してもよい。
推論・演繹としてのならば/よって/ゆえに/ということは
- 背理法: 「Aと仮定すると矛盾。ならばAでない」
- 場合分け: 「Aと仮定するとB。¬Aと仮定してもB。よってB」
- 三段論法: 「AとA→Bが示せた。よってB」
- 二重否定除去:「¬¬Aだ。ならば A。」
- ・・・
- これらは、推論規則と呼ばれる。いくつかの基本的な推論規則をベースに、それらを組み合わせた派生規則が無数に生み出される。
モデル版 ⊨ 「・・・という構造を決めるならば成立する/正しい」
- 「3つの元からなる集合を考えるならば互いに異なる二つの元が存在する」のように使う。公理を与えるのではなく、対象や演算の性質を具体的に定めることにより、文の成立不成立を議論する。意味論・モデル論的なアプローチ。
- 数理論理学では ⊨ を使い、左辺に構造を配置する M ⊨ ∃x∃y¬(x=y)
帰結版 ⊨ 「・・・が成立するならば・・・が帰結する」
- 「Aが成立するならば Bが成立するのように使う。前述の⇒と似ているが意味が限定されており、背後に特定の構造（およびそれによって定まる理論）を背景にある。しかし、我々が（通常の用途で）「⇒」や「ならば」を利用するときには、特定の構造を前提とするのが普通なので、⇒ と同一視してもいいのかもしれない。A ⊨ B のように使う

2. ならばに関するトピック

2-1. 演繹定理

「A⊢B(つまり Aを仮定するならばBが証明できる)」を「A → B が証明できる」と同一視してよいことを保証するのが演繹定理。演繹定理が成立しない場合もあるけれど、普通の数学では成立する。概念的に異なる → と ⊢ を（ある意味で）同一視しても、変なことにはならないことを主張。

「定理における日本語のならば、つまり $\Longrightarrow$ 」を「 ⊢ 」として解釈できる場合「A$\Longrightarrow$B」という言明は、演繹定理により「A→B」が定理であると解釈することができることを示している。

A$\Longrightarrow$B : 日本語(自然言語)を使った言明
A⊢B : 数理論理学を使ったメタレベルの言明
A → B: 数理論理学を使ったオブジェクトレベルの言明

2-2. 完全性定理

「T ⊢ A（Tを公理としてAが証明できる）」を「T ⊨ A (Tが成立するときには Aが成立する)」と同一視してよいことを保証するのが完全性定理。完全性定理が成立しない場合もあるけれど、普通の数学では成立するので、概念的に異なる ⊨ と ⊢ を同一視しても、変なことにはならない。（注：ゲーデルの不完全性定理とはまた別の話）

以上2-1.2-2 より、以下は通常同一視して構わない:

Aを仮定するならばBが証明できる
Aが成立するならばBが成立する
A→Bが証明できる
A→Bが成立する

2-3. 対偶証明

対偶証明と呼ばれる論法は、前述の演繹定理を使って正当化できる。つまり、「AならばBが成立する」は「A→Bが成立する」と言い換えてよい。あとは真理値表を使うと、「¬B→¬Aが成立する」と言い換えてよく、これに再度演繹定理を使えば「¬Bならば¬Aが成立する」と同一視できる。

2-4. 可証性述語

既にみたように、「AならばB」というメタな文は A→B というオブジェクトレベルの文に変換できる。では同様に「Tを仮定するならばAは証明可能」というメタな文でのならば＝「 ⊢ 」はオブジェクトレベルに落とし込めるのだろうか？

答えはできる場合とできない場合がある。ペアノ算術や集合論では可能。可証性述語Prとよばれ。不完全性定理への第一歩。

可証性述語を使うと、演繹定理を形式化できる（論理式として書ける）。つまり、形式化された演繹定理は PrA("B") ↔ Pr("A→B") ここで PrA は議論の土台となっている理論にAを定理として組み込んだ理論における可証性述語であり、クォーテーション"で囲まれた表現は、クォートされた論理式のゲーデル数を表す数である。

3. 参考文献とまとめ

菊池『不完全性定理』の2章と9章において、→の真理値表が納得がいきにくい理由を論じていたり、→を定理に ⊢ を証明を対応付けて考察しており、大いに刺激を受けた。また標準的な論理学の教科書でも、ここに記載されていることがある程度考察されている。例えば野矢『論理学』。

コメントや議論はウェルカムです。

「ならば」と 数学