この数学エッセーでは, 数学の証明の無駄の省き方について,
数学基礎論の立場で, 紹介します.
ここでは, 例として ZFC の公理系について論じますが, 他の形式的体系についても同様です.
実は, 数学では,
ZFC から命題 A を証明した時に, その証明に無駄があるかないかを,
さらに, その証明に無駄がある場合, その無駄を, 機械的アルゴリズムによって,
系統的に削除できます.
数学の論理では, すでにそれらのアルゴリズムが確立されています.
具体的にいうと, 最も重要なものが, LK におけるカット消去定理です.
ZFC から命題 A を証明した時, その証明図 P を LK 方式で書き下します.
P の終式 S は, ZFC の公理の有限個 B_1, … , B_n に対する,
B_1, … , B_n → A
の形です.
P にカット消去のアルゴリズムを適用し, 終式 S を変えずに,
カットのなしの証明図 P_1 ができます.
この時, P_1 が, ZFC から A を証明するための, 無駄のない証明図です.
P にどれだけの無駄があるかは, P に現れる, カットの推論図の個数で判定されます.
カットの推論図が多ければ多いほど, 無駄が多いです.
ここで, カットという推論図は, 俗にいう, 三段論法です.
数学の証明では, カットは, 無駄とみなされます.
なぜかというと, カットを使用することにより,
証明に, 本来必要のない論理式 (数学的文章) が紛れ込むからです.
逆に, カットのない証明図は, 終式の証明に必要のない論理式は,
一切紛れ込んでいないため, 無駄がないとみなされます.
さらに, 終式 S に現れない関数記号や述語記号を, P_1 から系統的に削除する方法があります.
このための手順も具体的に確立されています.
(ZFC ではあまり意味がないかもしれませんが, 一般の形式的体系では重要なことです.)
つまり, 証明のためには, 証明したい目的の式 S に,
explicit に現れる概念のみが必要で,
そのほかの概念は, 厳密な立場では, 一切が無駄ということです.
以上が, 数学における, 証明の無駄の省き方, そして, 証明の無駄の量の判定の仕方です.
カット消去の具体的なアルゴリズム (手順) については, 例えば,
参考文献: 竹内外史, 八杉満利子『証明論入門』
に掲載されています.
文責: Dr. Kazuyoshi Katogi
