構成主義と実無限

しんじけ @shinjike

@Zahlangabeheft それだと、単に潜在的無限（可能無限）を対象化しただけになるのでは。（議論はフォローしてませんので間違えていると思いますが）

yyyy/mm/dd @Zahlangabeheft

@shinjike 文脈は https://t.co/dhkGjPot https://t.co/JLxbOS3N です．実無限概念のポイントを，無限を表わす（一階の）タームの導入ないし対象化と見る，という考えを前提してます．

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt ですです．まったくその通り．

ytb @ytb_at_twt

@shinjike @zahlangabeheft 潜在的無限って普通、数学的に対象化できませんよね？それが対象化できるならば、古典的な意味での潜在無限ではなくなり、「実無限」チックになる、それが構成的集合論での無限集合、みたいにも言えますね。

yyyy/mm/dd @Zahlangabeheft

@ytb_at_twt @shinjike まあ「実無限の対象化」さえ結局その無限集合を外延として持つような述語について語ることだ，というフレーゲ的な集合観を取るならば，潜在的無限を生み出す手続きについて語ることを「潜在無限の対象化」と言ってもよいでしょう．

しんじけ @shinjike

@ytb_at_twt @Zahlangabeheft 「対象化」のイミが問題ですね。先ほどの山田さんの説明で理解しました。「未完のプロセス」という言い方にひっかかったようです。実無限は完成されているものだと思うので。

しんじけ @shinjike

そっちは構成主義数学の方にかかっているので、いいのか。うーん。

しんじけ @shinjike

無限公理がらみの問題が気になる。

しんじけ @shinjike

構成的超準解析とかもあるしな・・。詳しくはまったく知らないけど、あれは、超準モデルが別ルートを解して、構成主義的なモデルと同値になるという話だったような。

ytb @ytb_at_twt

@shinjike @Zahlangabeheft 結局、構成的集合論における無限公理は、ωを帰納的に定義されるプログラム（自然数を0,1,2,…と出力し続ける）と見なし、それを対象として存在を認める、という主張になりますね。

ytb @ytb_at_twt

@shinjike @Zahlangabeheft 構成的型理論において、帰納的に定義されるデータ型の存在を認めるという主張とこの点でパラレルですね。

しんじけ @shinjike

@ytb_at_twt @Zahlangabeheft 帰納的に定義されるプログラムという点では、構成的な「未完成のプロセス」であり、その点では潜在的無限の側面を持つように見えます。そのωを一階の対象として導入することで、実無限を認めたことになるのかは、私には判断できないです。

しんじけ @shinjike

構成主義数学での帰納的定義ってどうなっているんだろ。

しんじけ @shinjike

しまった。Rathjen とか Aczel とかわさわさ論文が出てきたでござる。。。むりぽ。

しんじけ @shinjike

Thierry Coquandのスライド「構成的数学における無限対象」によると「無限対象を構文的記述に置き換えることで、構成的数学において無限対象を満足のいく仕方で表現できる」とあるな。http://t.co/vzJatw2e

しんじけ @shinjike

Peter Dybjer "Inductive definitions in type theory" http://t.co/lD0zjNna

しんじけ @shinjike

矢田部俊介「あいまい性と極限 ー 構成的素朴集合論における余帰納的対象の定義可能性」 http://t.co/OPHkGOdo 「潜在的無限」について述べておられました汗。

しんじけ @shinjike

はぅ。自分の授業準備が

yyyy/mm/dd @Zahlangabeheft

おっと，「そこで余帰納的定義ですよ」ですか？と思ったのにツイートし忘れていました．RT @ytb_at_twt …そのプログラムが無限ループを含み出力が未完であっても、そのことがプログラムを対象とした操作を許すことに影響しないみたいな。

yyyy/mm/dd @Zahlangabeheft

「構成主義と実無限」をトゥギャりました。 http://t.co/qq95FtmX

yyyy/mm/dd @Zahlangabeheft

@shinjike @ytb_at_twt とりあえずまとめておきました．http://t.co/qq95FtmX

ytb @ytb_at_twt

@Zahlangabeheft @shinjike おお、すごい！ありがとうございます。

しんじけ @shinjike

@Zahlangabeheft @ytb_at_twt おお、ありがとうごいます。

しんじけ @shinjike

「プログラムの対象化」の話は哲学的にも面白いし、そこの細部にやどるテクニックがいろいろ分析できれば、どのような前提（道具立て）でどれくらいの表現力が得られるのかというところまでわかるのだろう。勉強して実感が欲しいところ。

Ryota Akiyoshi（秋吉亮太） @georg_logic

CZFに帰納的定義を足すとものすごく強いのか，初めて知った．．．http://t.co/3BxufeHx