「人間の理解を超えた証明」は証明だろうか
2019年7月1日のコメントペーパーより。レジュメは古典述語論理。
コメント：「人間の理解を超えた証明」とは何なのだろうか。その価値判断をできない証明はあくまで形式的なものでしかなく、誰に向けたものかすらわからなくなっている。
回答：前エントリ
のもとになったリプライへの再リプライです。いや、疑念はおっしゃるとおりではあるんですが、簡単に片付けられない問題でもあるのです。
というのは、数学の証明についてはもともと、人間の理解とは関係なく形式的なものだからこそ、証明は重要なのだという考え方があるのです。つまり、機械的な手続きに任せるからこそ、人間の不注意や偏見から自由な正しい結論が得られる、という考え方です。前回紹介したハッキングの本 (また宣伝しますが)
の中では「ライプニッツ的な証明の理念」と呼ばれています。(それと対置されるのが「デカルト的な証明の理念」で、こちらはまさに、人間の「理解」をもたらすような証明こそがよい証明だという考え方です。)
というわけで、証明が機械化され「人間の理解を超えた証明」の登場が現実味を帯び始めた現在の状況は、証明の本来の理念が転倒しているわけではなく、むしろ、ライプニッツ的理念が高度に達成された状況と言うことができます。言い換えれば、まったく見当違いの方向へ進んでいるわけではないのです。もちろん、それはたんに「高度な達成」ではなく「過度な達成」かもしれません。いずれにせよ、たんに機械的な証明は証明ではないと退ければすむ話ではなく、長年構築されてきた「証明の理念」を慎重に再検討しなければならないのだと思います。
ついでに、さらに宣伝しておくと、上記のライプニッツとデカルトの対比は、ハッキングの最初期の論文ですでに取り上げられていて、この論文が (正しさは別として) べらぼうにおもしろいので、ぜひ読んでください。
の第13章、拙訳です。
