構成主義と実無限

ytb @ytb_at_twt

そういえば、野矢茂樹氏の本のせいか、日本でも「直観主義＝実無限の否定」と信じる人が多い。けれど、それは間違っていると思う。構成的数学の枠組みとなる直観主義論理上の集合論（CZFとか）は無限公理を含んでいるし、無限公理は実無限の存在を仮定してるというのはムリのない主張ではないか。

Yuko Murakami @yukoim

@ytb_at_twt 有限主義の中でもいろいろありますからね…

ytb @ytb_at_twt

@yukoim 明らかに実無限を否定している有限主義のバージョンって何かありましたっけ？

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt 野矢本を擁護したくはありませんが，「無限集合を表わす名辞を含む＝実無限の存在を仮定」というのはやや粗雑では．「実無限の存在を仮定する」とは，要素のすべてが「すでに完成している」ような無限集合の存在を仮定するという非形式的な「哲学的」主張であり，→

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt →これを強いてもう少しまともな主張として述べようとすると，「実無限の存在を仮定する＝ある無限集合上の量化文に対して二値原理が妥当すると仮定する」になるのだと思います．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt …といっても，もちろん「実無限を認めることのポイントは，無限集合を表わすタームを認めるという点に尽くされる」という意見もあり，この意味では「構成的数学でも実無限を認めている」と言うのは文句なく正しいです．ただそれは構成主義者が批判したものではないと．

ytb @ytb_at_twt

@Zahlangabeheft CZFの無限公理より、任意の自然数n に対しnを表現する数値\bar{n} \in \oemga となることは証明でき、つまり集合ωが全ての数値を含む無限集合なこと自体は証明可能で二値原理が働かないのは他の元についてですが、これでは不足でしょうか。

ytb @ytb_at_twt

@Zahlangabeheft というか、野矢先生はともかく、現代的な構成主義者で「実無限は認めない」みたいなことを言う人はいるんでしょうか。＞ただそれは構成主義者が批判したものではないと．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt 「任意の自然数n に対しnを表現する数値\bar{n} \in \oemga となること」を実無限の存在の仮定とは誰も言わないでしょう．\forall x \in \omega (Fx) という形の文に対して一般に二値原理が成り立つかどうかという問題です．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt ええと，クリスチャンにとっての「イエスは湖の上を歩いた」という主張みたいな扱いかもしれません…．

ytb @ytb_at_twt

@Zahlangabeheft ファジイな人間としては「ωが無限集合であることは確定的に真であるがωの全ての元が確定しているわけではない」と言いたい所ですが。ωのtotalityが確定しているのが「実無限」の定義なんですか。ついでにこれはダメットとかの定義なんですか？

ytb @ytb_at_twt

@Zahlangabeheft …つまり盲信している過激派がたくさんいるということですね！

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt 必ず超準数を含むωのようなものは実無限じゃないと思いますね．定義ではなく，実無限という捉え難い考えの一つの定式化が「ωのtotalityの確定＝ω上の量化文に対する二値原理の妥当性」なのだと思います．Elementsのダメットの説明は確かこんな感じかと．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt いや過激派は絶滅してるでしょ…と言いかけて，そういえばネルソンはガチだった，いやそれどころかよくよく話を聞くと集合の要素は形成途上にあると思っている人が結構多かった，と思い出したので，「湖の上」は言い過ぎたかもしれません．聖体拝領レベルか．

ytb @ytb_at_twt

@Zahlangabeheft もちろん、ωに含まれる超準元のフォームが確定されれば、その限りではないんでしょうねぇ。ちなみに実無限を認めるとは「無限集合を表わすタームを認めるという点に尽くされる」といっている論者ってどんな人なんですか？

ytb @ytb_at_twt

@Zahlangabeheft まぁネルソンは…。

ytb @ytb_at_twt

@Zahlangabeheft 後者の意味では「構成的数学でも実無限を認めている」というのは、非常にリーズナブルな解釈だと思いますよ…（構成的型理論で帰納的データ型はしっかりと定義されているように思われ、「確定的に定義されていない」というのは非常に抵抗がある）

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt すみません，「尽くされる」と言った人を知っているわけではないです（「…尽くされる，という意見もありうる」と書けばよかった）が，実無限のポイントが無限集合を表わすタームを認める点にあるという主張はokmt先生が『事典哲学の木』の項目「無限」で述べています．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt 「ωに含まれる超準元のフォームが確定されれば、その限りではないんでしょうねぇ」というのも（フォームが何なのか曖昧なまま言えば）多分その通りで，totalityが確定か否かより，意味論的な値が客観的に決まっているかどうかがより重要な区別になります．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt うーん，そもそも「実無限を認める／認めない＝無限集合を認める／認めない」という重ね合わせがよくないと思いますけどね…．実無限概念の分からなさをかみしめた上で，「要するに無限集合も対象ってことね」と押さえて，実無限概念にさよならするのがいいと思います．

ytb @ytb_at_twt

@Zahlangabeheft それはわかります。ただ、「実無限」にこだわるの人は「直観主義者」に多いんで、そちらへの対処はお任せします。

ytb @ytb_at_twt

@Zahlangabeheft okmt先生の項目は私も読みました。あれは素晴らしい記事だし、結論もリーズナブルだと思います。

yyyy/mm/dd @Zahlangabeheft

そうか，「構成的数学も実無限を認めている」と主張するのは，無限を「未完成のプロセス」と捉えることと，無限を「対象」として扱うことの両立可能性，すなわち「未完成のプロセスを対象化することは可能だ」ということを主張することになる…と言えば何だかありがたい感じになるな．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt 確かに，直観主義者にとって反‐実無限は一つの旗印ですからね．

ytb @ytb_at_twt

@Zahlangabeheft 無限集合を、それを出力するプログラムと同一視する（またプログラムを対象とした有限的な操作を許す）んじゃないでしょうか。そのプログラムが無限ループを含み出力が未完であっても、そのことがプログラムを対象とした操作を許すことに影響しないみたいな。