  |
はてなキーワード: 古典論理とは
↑new
「対象を具体的に構成することによって証明可能ならば, 存在しないと仮定して云々ではなく, 実際に構成したほうがよい」あるいは「(最狭義の)背理法なしでいけるならそうすべきだ」(これらは別の主張である)という主張なら意味は通りますが. もっともこの種の議論も教育云々に属すので.
彼の意味の非背理法証明は古典論理に従う通常の証明であり構成的証明や直観主義的な証明などとは異なる. だから直観主義的型理論の証明からrealizerとしてプログラムと正当性証明を抽出する話とか, 直観主義論理の存在具体化性なんかの話とは全く関係がない.
「機械的に書き換え可能なら情報量は変わらないのでは」という簡単な突っ込みもできる. 幾らかの人達は「とはいえ計算数学なんかでは背理法に依らない証明を考えるのは意味があるのでは」といったことを述べているが
件の著書の内容紹介に【「背理法による証明」を、格段に情報量の多い「背理法によらない証明」に機械的に書き換えることができる】とある. これは, 彼の意味の背理法による/よらない証明と, 古典論理/非古典論理による証明, または非構成的/構成的証明, との対比を混同している.
---
「LKもcut-free LKも非背理法的ということではないのか. そうだとするとカット除去定理は背理法除去とは無関係ではないのか.」
他方で彼の著書では竹内・八杉『証明論入門』を引用してカット除去定理が背理法除去を一般化した定理だとも主張している. ここでひとつ反論ができるとすれば「sequent calc.も非背理法的な証明体系ではないか. 証明に現れるsequentは全てvalidではないか.」
---
他方で彼のいう非背理法証明というのはそういう状況が起こらない証明をいう. Hilbert流の証明体系では途中にprovableなformulaしか現れないことを想像せよ. したがって彼の数学としての主張は「自然演繹とHilbert流の体系は同値. よって背理法は除去できる」
実際efqを用いた証明ではefqの適用の直前に矛盾が導かれているはずだから「途中に正しくない主張が現れる」という状況に適合している.
だから彼の拒否する証明法は広義の背理法よりももう少し広いものと考えられる. 例えばex falso quodlibetがnonsenseな証明法だと捉えていることは彼のサイトの記述から明らか.
正確にいうと彼のいう背理法は「否定導入と最狭義の背理法」を合わせたもの. 背理法を拒否する根拠は「背理法を用いた証明では途中に正しくない主張が現れる」こと. 自然演繹の証明図は途中にunprovableなformulaが現れることを想像せよ.
また「背理法を用いて証明できるなら用いないでも出来る」というのは彼の言葉の定義では正しいので「直観主義論理が云々, 派生規則だから暗黙に背理法が使われてる云々」は反駁にならない.
「教育の話だろ」という人間には「教育論の補強に数学を濫用しているし, 数理論理学の教科書まで出版している」と反駁しましょう.「それでも教育的な価値は云々」という人間には「教育論として批判しているのではなく数学として批判しているのだ」と反論しましょう.
適切に批判しないと「(最狭義の)背理法なしでは(通常の述語論理の形式的体系において)証明できない命題があるなどという人間は(彼の意味では背理法なしでも証明できるので)数理論理学を理解していない初心者である」などと云われて, 傾げる首を切り取られてしまった人間が賛同するので
トラバぐらいつけたらどうだ。
まず、ITは比較的斜陽ではない。ITが斜陽ならインフラ以外は皆斜陽だな。ああ、そういうことが言いたかったのなら気にしないでくれ。
つまりは国語教育を何とかしろ、ということだろう？それならまずディベートやグループディスカッションをさせればいい。今の教育は「こんな議論の形式があります」って教えるだけだからな。小論文や説明文は夏季休業時の宿題にしてもいいだろう。このうちから10000字以上の文章生産性を向上させる訓練はしていていいはずだ。
個人的には古文漢文は今の学習量の半分でいいと思っている。削減して生まれた余裕のうち何割かをそこに当てればいいだろう（個人的には言語学的要素をもう少し増やしたいが、皆必要というわけではないからそれはなくてもいい）
私立大学は早慶以外全部潰せ、と書いたはずだ。すなわちそれを学ばないやつは大学に来る必要がない、ということ。そこまで徹底すれば高校も必修にせざるを得ない。なぜならそれを学ばない＝バカが通う高校という社会的評価が下されるからな。そういうところはどんどん潰れる。
ちなみに論理は古典論理か、述語論理か。まさか様相論理までさせるわけではあるまい。
統計というか、「表や図の作成、理解とその分析」は必須だろうな。ただそれを一教科作ってまでやるというのは難しいだろう。
たとえば夏季休業に社会科学統計（地歴公民）か自然科学統計（統計）のどちらかを分析させることを宿題に出すのはどうだろう。もちろん該当する科目でそれぞれ一度は分析を経験した上で、だ。
> だから、「数理経済学だからゲーム理論家じゃない」って思ってるお前が馬鹿ってことでしょ。
おいおい「ピュアな」を忘れんなよ。統計の著作なんて一個も無いはずだよなあ？
> あと、無税国家になるって経路かインフレが実現されるかってので、筋書き違うだろ。
ほんとに論理学わかって無いなあ。
・どちらでもうれしい結論
と言ってるのに、それに対する反論になってないだろ。
> 文献精読
どうでもいいから「国債を買い捲ればデフレ脱出必ずできる（のにやらない日銀は馬鹿）」っていう命題が「バーナンキの背理法」かどうかぐらいは確認しろよ。
> for-allで「必ず」ってのは入ってるじゃねえか。一意はよけいだけど、まあ背反はしない。（for allならたくさんあって、そのなかの全て、uniqueなら、ひとつしかなくて、そのなかの全て。）てめえこそ、論理構造をもう一回見て来い。
for-allは∀ですが、古典論理で「必ず」なんていう限量子があるんですかｗｗ どう書くんですかｗｗ
それとも、あなたのケイザイガク論文では様相論理でも使ってるんですかｗｗ
「論理構造」っていうタームがあるんですかｗｗ 定義は何ですかｗｗ
あれはいい本だけどさあ。ここで君が権威付けに持ち出すには初歩的過ぎるだろｗ
