  |
↑new
「対象を具体的に構成することによって証明可能ならば, 存在しないと仮定して云々ではなく, 実際に構成したほうがよい」あるいは「(最狭義の)背理法なしでいけるならそうすべきだ」(これらは別の主張である)という主張なら意味は通りますが. もっともこの種の議論も教育云々に属すので.
彼の意味の非背理法証明は古典論理に従う通常の証明であり構成的証明や直観主義的な証明などとは異なる. だから直観主義的型理論の証明からrealizerとしてプログラムと正当性証明を抽出する話とか, 直観主義論理の存在具体化性なんかの話とは全く関係がない.
「機械的に書き換え可能なら情報量は変わらないのでは」という簡単な突っ込みもできる. 幾らかの人達は「とはいえ計算数学なんかでは背理法に依らない証明を考えるのは意味があるのでは」といったことを述べているが
件の著書の内容紹介に【「背理法による証明」を、格段に情報量の多い「背理法によらない証明」に機械的に書き換えることができる】とある. これは, 彼の意味の背理法による/よらない証明と, 古典論理/非古典論理による証明, または非構成的/構成的証明, との対比を混同している.
---
「LKもcut-free LKも非背理法的ということではないのか. そうだとするとカット除去定理は背理法除去とは無関係ではないのか.」
他方で彼の著書では竹内・八杉『証明論入門』を引用してカット除去定理が背理法除去を一般化した定理だとも主張している. ここでひとつ反論ができるとすれば「sequent calc.も非背理法的な証明体系ではないか. 証明に現れるsequentは全てvalidではないか.」
---
他方で彼のいう非背理法証明というのはそういう状況が起こらない証明をいう. Hilbert流の証明体系では途中にprovableなformulaしか現れないことを想像せよ. したがって彼の数学としての主張は「自然演繹とHilbert流の体系は同値. よって背理法は除去できる」
実際efqを用いた証明ではefqの適用の直前に矛盾が導かれているはずだから「途中に正しくない主張が現れる」という状況に適合している.
だから彼の拒否する証明法は広義の背理法よりももう少し広いものと考えられる. 例えばex falso quodlibetがnonsenseな証明法だと捉えていることは彼のサイトの記述から明らか.
正確にいうと彼のいう背理法は「否定導入と最狭義の背理法」を合わせたもの. 背理法を拒否する根拠は「背理法を用いた証明では途中に正しくない主張が現れる」こと. 自然演繹の証明図は途中にunprovableなformulaが現れることを想像せよ.
また「背理法を用いて証明できるなら用いないでも出来る」というのは彼の言葉の定義では正しいので「直観主義論理が云々, 派生規則だから暗黙に背理法が使われてる云々」は反駁にならない.
「教育の話だろ」という人間には「教育論の補強に数学を濫用しているし, 数理論理学の教科書まで出版している」と反駁しましょう.「それでも教育的な価値は云々」という人間には「教育論として批判しているのではなく数学として批判しているのだ」と反論しましょう.
適切に批判しないと「(最狭義の)背理法なしでは(通常の述語論理の形式的体系において)証明できない命題があるなどという人間は(彼の意味では背理法なしでも証明できるので)数理論理学を理解していない初心者である」などと云われて, 傾げる首を切り取られてしまった人間が賛同するので
13
