kazz の数学旅行記

数学の話題を中心に, 日々の知的活動の旅路を紹介します.

数学の証明の無駄の省き方 (LK におけるカット消去)

この数学知恵ノートでは, 数学の証明の無駄の省き方について, 

 

数学基礎論の立場で, 紹介します.

 

 

 

ここでは, 例として 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