  |
はてなキーワード: 直観主義とは
重要な点は"最初に"、「0.99....が数であるとした時点で必ず1になってしまう」こと自体を納得させることだと思いますよ。
その上で、0.99....のようなものでも同種の数となるように"作られた"のが実数である、という話にすればいいでしょう。
無知の状態から認識をもたせる上では、(数学書のように)先に一般化した条件を証明してあとで具体論で確認させる手順こそが問題です。かんたんに一般化された定理のほうへ話をすすめてはいけません。
----
もちろん「1以外のすべての数」でない数は1だけ、というのが論理として正しいか、というところには疑問の余地があって、そうとはいえないとするのが直観主義で、直観主義の立場を取るなら実数など認められないという話になるわけです。
ただ実数を認めないなら平方根や円周率を含む中学数学自体もみとめられないことになるので、この場ではそうではない実数を認めなくてはいけない立場にある、でよいのではないでしょうか。
デカルト閉圏というものがある。これは型付きλ計算や直観主義論理のモデルとなる圏だけども、その特徴は
である。これらをプログラムに対応させると次のようになるだろう。
| 終対象 | unit |
| 直積 | 直積型 |
| 冪 | 関数の型 |
| - | 双対概念 | プログラムへの対応 |
| 終対象 | 始対象 | 終了しない計算(例外) |
| 直積 | 直和 | 判別共用体 |
| 冪 | 余冪 | ??? |
余冪に対応するものがよく分からん。余冪の定義からいうと余冪を X**Y と表現することにすれば
Hom(X**Y, Z)≅Hom(X, Y⊕Z)
が成立すればよい。だから、
IntOrString = IntValue of int | StringValue of string let f(x:int) : IntOrString = if x >= 2 then IntValue(1) else StringValue("1")
let f'(xy:X**Y) : string = "1"
のように書き換えることができればそれは余冪と言えると思えるのだが、そのような書き換えは可能なのか？
とりあえずこの場合に限れば、
exception Y of int
type XToYCopower(x:int) =
let x' = if x >= 2 then raise(Y(1)) else x
let f'(xy:XToYCopower) = "1"
みたいにして、呼び出すときは、
let mutable z: IntOrString = IntValue(0) try z <- StringValue(f'(XToYCopower(0))) with | Y(y) -> z <- IntValue(y)
とすると、書き換えができているような気もするし、やはり何か違う気もする。
よく分からんなぁ…。
↑new
「対象を具体的に構成することによって証明可能ならば, 存在しないと仮定して云々ではなく, 実際に構成したほうがよい」あるいは「(最狭義の)背理法なしでいけるならそうすべきだ」(これらは別の主張である)という主張なら意味は通りますが. もっともこの種の議論も教育云々に属すので.
彼の意味の非背理法証明は古典論理に従う通常の証明であり構成的証明や直観主義的な証明などとは異なる. だから直観主義的型理論の証明からrealizerとしてプログラムと正当性証明を抽出する話とか, 直観主義論理の存在具体化性なんかの話とは全く関係がない.
「機械的に書き換え可能なら情報量は変わらないのでは」という簡単な突っ込みもできる. 幾らかの人達は「とはいえ計算数学なんかでは背理法に依らない証明を考えるのは意味があるのでは」といったことを述べているが
件の著書の内容紹介に【「背理法による証明」を、格段に情報量の多い「背理法によらない証明」に機械的に書き換えることができる】とある. これは, 彼の意味の背理法による/よらない証明と, 古典論理/非古典論理による証明, または非構成的/構成的証明, との対比を混同している.
---
「LKもcut-free LKも非背理法的ということではないのか. そうだとするとカット除去定理は背理法除去とは無関係ではないのか.」
他方で彼の著書では竹内・八杉『証明論入門』を引用してカット除去定理が背理法除去を一般化した定理だとも主張している. ここでひとつ反論ができるとすれば「sequent calc.も非背理法的な証明体系ではないか. 証明に現れるsequentは全てvalidではないか.」
---
他方で彼のいう非背理法証明というのはそういう状況が起こらない証明をいう. Hilbert流の証明体系では途中にprovableなformulaしか現れないことを想像せよ. したがって彼の数学としての主張は「自然演繹とHilbert流の体系は同値. よって背理法は除去できる」
実際efqを用いた証明ではefqの適用の直前に矛盾が導かれているはずだから「途中に正しくない主張が現れる」という状況に適合している.
だから彼の拒否する証明法は広義の背理法よりももう少し広いものと考えられる. 例えばex falso quodlibetがnonsenseな証明法だと捉えていることは彼のサイトの記述から明らか.
正確にいうと彼のいう背理法は「否定導入と最狭義の背理法」を合わせたもの. 背理法を拒否する根拠は「背理法を用いた証明では途中に正しくない主張が現れる」こと. 自然演繹の証明図は途中にunprovableなformulaが現れることを想像せよ.
また「背理法を用いて証明できるなら用いないでも出来る」というのは彼の言葉の定義では正しいので「直観主義論理が云々, 派生規則だから暗黙に背理法が使われてる云々」は反駁にならない.
「教育の話だろ」という人間には「教育論の補強に数学を濫用しているし, 数理論理学の教科書まで出版している」と反駁しましょう.「それでも教育的な価値は云々」という人間には「教育論として批判しているのではなく数学として批判しているのだ」と反論しましょう.
適切に批判しないと「(最狭義の)背理法なしでは(通常の述語論理の形式的体系において)証明できない命題があるなどという人間は(彼の意味では背理法なしでも証明できるので)数理論理学を理解していない初心者である」などと云われて, 傾げる首を切り取られてしまった人間が賛同するので