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

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