不完全性定理は「現代科学の限界」なるものを示してはいない（その１つづき）

数学

これまでのお話

第二不完全性定理は「体系は自身の正しさを証明できない」ではない

今日、第二不完全性定理として知られている定理は、次のものです。


体系 T が以下の三条件をみたしているとする。
  1. T は PA を含む。
  2. T は帰納的に記述できる。
  3. T は無矛盾である。
このとき、Con(T) は T で証明可能でない。


前提にも結論にも、論理式や体系の真偽に関する条件は含まれていません。つまり、第二不完全性定理のステートメントには真偽概念は含まれていません。これは、前回見た第一不完全性定理と同じ事情です。

ここで、前提の三条件は第一不完全性定理のものと同じですので、真偽概念を含まないことは前回に確認済みです。念のため、再掲しましょう。

体系 T が体系 t を含むとは、体系 t の論理式 A を体系 T の論理式 A* に翻訳し、さらに、A に t での証明 Π があれば体系 T における A* の証明 Π* に翻訳する、翻訳手続き * が存在することです。

PA は一階ペアノ算術の略称で、自然数論の体系の一つです。コンピュータで計算できる関数はすべて定義でき、さらに多くの関数が定義でき、数学的帰納法は自由に使えますが、無限集合は扱えない程度のものです。

帰納的に記述できるというのは、次の二条件が成り立つことです。

  1. 論理式 A が与えられたとき、A が公理であるかどうかを判定する手続きが存在する。
  2. 論理式 A1, …, An, B が与えられたとき、A1, …, An から B を導くことが推論規則の正しい適用であるかどうかを判定する手続きが存在する。
形式的体系における証明とは、公理から出発して推論規則の適用を有限回行なうことですから、この二条件は、その体系のための証明検証系（証明らしいものが与えらたとき、それが正しい証明であるかどこかに間違いがあるかを検証するプログラム）を、（原理的には）書くことができることと、同値です。自動証明系（定理を与えるとその証明を構成するプログラム）を書くことができる必要はありません。

なお、PA も帰納的に記述できる体系です。実用的な体系の多くは帰納的に記述できます。帰納的に記述できない体系も存在します。

体系が矛盾するとは、ある論理式 A とその否定 ¬A がどちらも証明できることです。体系が無矛盾であるとは、矛盾しないことです。

以下、T は前提の三条件をみたす体系とします。

T は帰納的なので、論理式の並び S が論理式 C の証明であるかどうかを判定するプログラムを書くことは原理的には可能です。以下を確認すれば良いからです。

  • C に現れるすべての論理式 Ai について、以下のいずれかが成り立つ。
    • Ai は公理である。
    • Ai よりも前に現れる論理式 Aj1, ..., Ajn をうまく選ぶと、Aj1, ..., Ajn から Ai を導くことは推論規則の正しい適用である。
  • S は C で終る。

よく知られているように、コンピュータはすべてのデータを内部ではビット列(0と1の並び)で表現しています。たとえば、この文書も、HTMLテキスト(あるいは、HTMLテキストに自動的に変換できる何か)としてサーバのディスクにファイルとして格納されていて、ファイルの中身は本質的には長いビット列です。ビット列は非負整数の二進表現とみなすことができます。つまり、コンピュータの扱うことができるデータは、すべて、大きな整数として表現されます。

ということは、論理式の並び S が論理式 C の証明であるかどうかを判定するプログラムは、整数 x と整数 y を入力すると、x の表現する論理式の並び S が y の表現する論理式 C の証明であれば「真」を、そうでなければ「偽」を出力する関数を実装しているということです。難しくはないが長くて面倒なテクニカルな議論をすると、この関数は PA の論理式で表現できることを示すことができます。その論理式を Proof(x, y) と書くことにしましょう。

論理式 C が証明可能であるとは、「ある論理式の並び S が存在し、S は C の証明である」ことです。これに対応する整数についての論理式は、PA で (∃x)Proof(x, y) と書くことができます。これを判定するプログラムは書くことができないことがわかっていますが、PAの論理式として表現するだけなら困りません。

体系 T が矛盾するとは、「ある論理式 C が存在して、C も ¬C も証明可能である」ことです。体系 T が無矛盾であるとはその否定のことです。したがって、体系 T が無矛盾であることに対応する PA の論理式は、

¬(∃y)((∃x)Proof(x, y)∧(∃y')(Neg(y, y')∧(∃x')Proof(x', y)))
と書くことができます。これを、Con(T) と略記します。ただし、Neg(y, y') は、「y が論理式 C を表現するなら、y' は ¬C を表現する」に対応する PA の論理式です。

ところで、T は PA を含みます。つまり、PA の論理式を T の論理式に変換する規則が存在します。したがって、Con(T) を T の論理式に変換することができるはずです。本来は別の記号を使うべきところですが、通常は混乱のおそれはないので、Con(T) を T の論理式に変換したものも、Con(T) と書きます。

第二不完全性定理の結論は、このように定義される Con(T) が T で証明できないということです。ここに、 Con(T) の真偽に関わることは一切出てきませんし、T の各公理に真偽に関わることも出てきません。

結論に真偽概念が含まれていないことがわかりました。

第二不完全性定理でも、前提の三条件も結論も、ソフトウェアの言葉でいえば記号処理のみで定義できる条件であることがわかります。数理論理学の言葉では、第二不完全性定理も、純粋に構文論的に記述できる定理であり、体系の真偽には依存しないことがわかるはずです。第一不完全性定理とまったく同じ事情です。

(次回未定)