今回の数学エッセーでは, 数学の中では, 幾分通俗的な記事を書いてみます.
テーマは, 『背理法は必要か?』
ここで言う背理法とは, 論理式 A に対し, not A を仮定して矛盾が出たら, A が証明可能であると主張する原理です.
結論を言うと, 数理論理学に, 以下の基本定理があります:
『背理法を使って証明できる定理は, 背理法を使わなくても証明できる.』
もっと詳しく言うと, 背理法を使った証明は, 背理法を使わない証明に書き換えができるのです.
この超数学的定理は, LK や LJ を定式化したゲンツェンの基本定理 (カット消去定理) の特別な場合です.
つまり, カット (三段論法) を使って証明できる sequent は, カットを使わなくても証明できると言うものです. (詳しくは, カットを使った証明図は, end sequent を変えずに, カットを使わない証明図に書き換えができると言うものです.)
背理法だけではなく, 対偶を取って証明できれば対偶を取らなくても証明できるとか,
カット消去定理にはさまざまな応用があります ([1]).
東京理科大学のある先生が, 背理法は必要ないとおっしゃっていたのは,
このカット消去定理をご存知だったのでしょうね.
参考文献
文責: Dr. Kazuyoshi Katogi
