ある掲示板で話題になっていました.
その掲示板での説明が, 私にはわかりにくかったので,
今回の数学エッセーでは, 論理式 A に対し,
(A ⇒ ￢A) ∧ (￢A ⇒ A)
から矛盾が導かれることの証明を, LJ で与えます.
(A ⇒ ￢A) ∧ (￢A ⇒ A) を R と略記します.
ここに, A ⇒ B は『A ならば B』の意味で,
論理式の列 S: A_1, ..., A_n
と
論理式 B
に対して, S を左辺, B を右辺に持つ sequent を
S → B
で表すことにします.
sequent
R →
の LJ に於ける証明図は以下の通りになります:
(図 1の通り)となります.
(表示するデバイスによっては文字化けで正しく表示できないので,
スクリーンショットを撮って, 画像で表示しています.)
ここに, (1)～(16) は, 以下の sequent です:
(1) A, A ⇒ ￢A → A
(2) ￢A, A, A ⇒ ￢A →
(3) A, A ⇒ ￢A → ￢A
(4) A, A ⇒ ￢A →
(5) A ⇒ ￢A → ￢A
(6) ￢A , ￢A ⇒ A → A
(7) ￢A, ￢A, ￢A ⇒ A → A
(8) ￢A, ￢A ⇒ A →
(9) ￢A ⇒ A → ￢￢A
(10) R → A ⇒ ￢A
(11) R → ￢A
(12) R → ￢A ⇒ A
(13) R → ￢￢A
(14) ￢￢A, R →
(15) R, R →
(16) R →
ここで, sequent (1), (3), (6), (10), (12) は明らかに LJ provable
なので, その部分の証明図は省略しました.
また, 増・減などの推論で, 自明にわかる部分は省略しました.
一方, LJ からは排中律は証明不可能です.
従って, 以上のことにより, R から矛盾を導くのに, 排中律は必要ありません.
文責: Dr. Kazuyoshi Katogi
