つづき

この矛盾の意味は¬C∈Γであるか、C→¬Aであるかです。
Γ（ガンマ）自体は無矛盾の前提ですし、"A→B→C"の中に現れる命題A・B・Cは全てΓ∧A・Γ∧B・Γ∧Cの省略の意味ですから、対偶（NJ・NKでは対偶の規則も成り立つ）によってBはΓと矛盾することが分かります。

つまりA・B・Cが命題として切り取られている限りΓの解釈ではBは間違いであるとわかります。
またこのことから、（細かい議論は抜きにして）背理法から直接証明に書き換えることも可能であるとわかると同時に、直接証明から背理法に書き換えることも同じく可能であることはすぐに理解されるでしょう。

以上のことから、「背理法が意味内容の決定できない副産物を生み出すから内容が理解できない」という主張は誤りであるとはっきりと指摘できる上に、脱背理法論者が"素晴らしい直接証明"と紹介している証明も背理法の形式に書きなおすことが出来ます。
書き換えた場合は当然に、使っている命題はリテラルでみて肯定と否定の対が入れ替わる箇所がありますが、"材料"は同じですから本質的に意味内容は変わりません。つまり"素晴らしい直接証明"とやらを"素晴らしい背理法"に書き換えられるということです。

(以上の議論はΓを素朴に集合とみなして∈を無神経に使ったりと正確でない部分がありますが、わかりやすさ重視のためにこのようにさせていただきました。）

因みに、名称は一貫してはいませんが、NK（またはNJ）の推論規則では、

・NJとNKの範囲における否定の導入
　　　A→矛盾　⇒　¬A
・NKの範囲における二重否定の除去
　　　¬A→矛盾→¬¬A　⇒　A

の何れか、あるいは両方をまとめたものを背理法と呼ぶことがあります。
この場合は推論規則としての背理法という呼称ですから、数学全般における証明技法としての背理法とは別の概念であるということも大事なことです。

つづく