我々は, 高校数学で, √2 が無理数であることの, 帰謬法による証明を習います.
推論の中核を言葉で書くと, 以下のようになります:
『√2が有理数と仮定して矛盾が出た. 従って, √2 は無理数である.』
しかし, この推論は, 論理的には, 帰謬法ではありません.
実数の全体を R, 有理数の全体を Q, 無理数の全体を I として,
証明の大まかな流れを LK 方式で書いてみると,
ZFC, √2 ∈ Q →
--------------------------- ・・・・・・・・・・・・・・・・・・・(1)
ZFC → ¬ √2 ∈ Q, ZFC → √2 ∈ R
-------------------------------------------------------------------
ZFC → √2 ∈ R ∧ ¬ √2 ∈ Q
----------------------------------------
ZFC → √2 ∈ I
となります.
つまり, ZFC に於いて, √2 ∈ Q を明示的公理として追加して矛盾を導くわけですね.
(I := R - Q として定義されます. )
ここで, (1) の推論は, 帰謬法ではなく, 単なる ¬ 右です.
ちなみに, ZFC に於ける帰謬法というのは, LK 方式で書いてみると,
ZFC, ¬A →
------------------- ・・・・・・・・・・・・・・・・・(2)
ZFC → A
の形の推論のことです.
推論 (2) に於いて, LK では, 上式から下式へ移行する際には,
大概は, cut を使わなくてはなりません.
文責: Dr. 加藤木 一好