で、ブルバキをきちんと読まないのにコメントするのはおかしいとは思うのですが、数学を集合論的に規定された構造を扱う学問だ、という考え自体はそれなりに価値のある考えだと思います。ただ、私は数学の「構造」を規定している「集合」概念を、公理的集合論が与えている一階の構造として規定するのはあまり説得力を感じません。もちろん、それらの「近似」として公理的集合論を研究することには十分意味があるとは思います。個人的な意見ですが、数学で直観的に扱われている集合概念としてはMartin LeofのIntuitionistic type theoryが一番美しい(かつ哲学的な正当化が示されている)と思っています。もっとも、おそらくいろいろな公理的集合論と等価性が示される可能性が十分あるとも思っていますが。
まず傲慢な言い方かも知れませんが、実際に数学に対して創造的な貢献をする能力という点からみて、私は数学に対して十分な理解をもっていると自負しています。そして、「構成的でない数学は無意味」と(すくなくとも今の段階では)考えています。それから、「構成主義」は反動主義ではなく、むしろ哲学的により説得力があると同時に、数学的により豊かな内実をもっていうのが私の意見です。
付け加えて言うと、集合論者の言うところの具体性は私には単なる印象論にすぎないように見えます。集合論の内容が具体的なのではなく、「集合が具体的な対象である」という信仰が存在する、ということに過ぎないように思えるのです。非実用的な数学を擁護するコンテキストで、数学者が数学者が「見えるんだなあー」と言っているのと同じ神秘主義に過ぎません。一方、構成主義は「構成」という概念に対して明確な定式化を与えています。これだけから見ても、どちらが生産的な研究プログラムであるかは明らかです。学問的な内容の豊かさは、その学問が仮定する存在者の量によるのではなく、まずその学問が対象とするべき基本的な対象(私の意見では、自然数や実数など)についてどれだけ深い理解が得られるかで図られるべきです。
にもかかわらず、構成主義が「反動的」と受け取られるのは、ヒルベルトの「排中律を数学から排除するのはボクサーからこぶしを取り上げるもの」というような誤解がいまだに残っているからだと思います。実際には古典的な数学の大半は構成的に解釈が可能です。「まだ」うまくいっていないのは、排中律と選択公理が組み合わさったような場合ですが、これについてもいろいろと研究されています。
付言しておくと、私も「非構成的な数学を研究することが無意味」と考えているわけではありません。というのも、いずれこれらもまともな「数学」である限り構成的な意味づけが与えられると考えているからです。(形式的体系での導出可能性についての言明としては常に解釈可能です。が、もっとましなものがあると信じています。)そして、構成的な証明の方が豊かな内容を持つ分、証明を得ることが困難であり、便法として古典的な証明も認められると考えています。
ところで、「計算機科学的な立場から」云々と仰られていますが、このように専攻分野(やひどい場合になると指導教授で)色分けして議論することが日本の学問のレベルを著しく低下させていると思います。学問的な言説は学問的な内容に即して判断されるべきです。ちなみに私は数学プロパーです。(1年ほど哲学科にいましたが。)
実は私も自分のWebサイトで構成主義数学を実際に展開しているので、ちょっと意見を述べてみたいと思います。
私は、昔BishopのFoundation of constructive analysis を読んで、排中律無しでルベーグ式の積分論が展開できるとか、ハール測度が構成できるとか、リーマンの開写像定理が証明できるなどの事実を知って驚愕しました。
ただし、Bishopは、その構成主義数学の公理や推論規則を明示的に提示しなかったので、その構成主義に則った数学の、形式主義という観点からの根拠付けが一体どうなっているのかについてずっと疑問で、自分なりに考えぬいた末、「メタ数学的な意味で根拠のある推論規則や公理しか仮定しない数学が構成主義数学である」ことを知って再び驚きました（その具体的な解説は、↑のURLで解説しています）。確かにyoriyukiさんのおっしゃるように、構成主義数学には「推論の出発点であるはずの、公理や推論規則にも明確な根拠がある」のです。それも“哲学的”なアヤシい議論ではなく、超数学的な、明確に数学的な議論によってです。
更に言えば、このような観点から見ると、選択公理は全然非構成的な公理ではなく、ZFCの公理の中では、意外にも「外延性公理」が一番非構成的な公理であるということができます（事実、Bishopの本では外延性公理は仮定せず、選択公理は仮定しています）。これはなぜかというと、ゲンツェンの自然推論の「消去規則」というのは、構成主義的観点からすると、「導入規則」から一意的に定まるものであり、等号についても「T=T」が導入規則とすると、これから一意的に定まる消去規則は「P(S) と S=T から P(T) が導ける」なのです。
ところが、外延性公理というのは、「AとBの元が共通である」ときに「A=B」を導いてしまう公理なので、一種の「等号の導入規則」であるとみなすことができます。すると、これに対応して（構成主義的な意味で）一意的に定まる消去規則は最早「P(S) と S=T から P(T) が導ける」ではなく、本来ならこの推論規則を捨て、外延性公理に対応する推論規則に置き換えなければならないはずなのに、通常のZFCの推論体系ではそれをしていないからです。
さて、とはいうものの、非構成的な数学が無意味かというと、そうではなくて、構成的な数学の、ある種の「近似理論」として意味があると考えています。
それだけでなく、コンパクト性とか、超フィルターの存在定理などは、バーチャルな世界の大変面白い議論として個人的には大好きです。でもしかし、このような排中律を本質的に用いた数学の議論を読んでいるときは、全然リアリティーを感じなくなってしまっていることもまた事実ですが…。
yoriyukiさんこんばんは。ちょっと誤解されているのではないかと。
まず選択公理と正則の公理に関しては、全くコンテキスト違いです。こちらは気になされていないようなので、どうでもよいのでしょうが。
「構成主義」に対する批判めいたことを書いたのは、こちらはご推察の通り、くるるさんのところの議論から誘発された面があることは事実です。さらにヒルベルトの有限基底定理に関して、どうしてこのような醜い定式化を行うのか、という感想を抱いたことも確かです。ですが、構成主義のみを許す観点に対する批判と yoriyukiさんとは全然関係ないです。そもそも yoriyukiさんが「構成的でない数学は無意味」と考えられているかどうかなど知る由もありません。上で言及した議論に対する一般的な感想という面、最近読み直した「廣瀬健・横田一正著 ゲーデルの世界」の内容に関してかなり違和感を持った (もっともこの本はゲーデル原論文の翻訳の価値がすばらしいのですが) こととか、別コンテキストその他の事情なり色々混じってるのです。その辺りを明確にしなかったため、ご不快な思いをされたのでしたらおわび致します。
で、肝心の構成的な数学に関してですが、yoriyukiさんが最初の方で「構成的でない数学は無意味」と書かれていますし、最後の方では「非構成的な数学を研究することが無意味」と考えられているわけではないと記載されていますので、良く分かりませんが、もし構成的でない部分を認められないというのでしたら、そちらには同意しかねるということは事実です。
さらに「計算機理論 (計算理論ではない) や 工学的視点からの偏見」という記述は、一般論としても上品ではなかったと思います。これは上のゲーデル本の違和感に誘発されて書いたのですが、逆に自分自身の工学等に対する偏見が出てしまったというのが本当のところだと思います。
Stromdorfさんこんばんは。どうもお久しぶりです。Stromdorf のところの掲示板でもちょっと話題になっていましたが、私の環境ですと数式の閲覧が難しく、一度真面目に読ませて頂こうと思いつつ、数式以外の部分を読んでいる状況なのは、誠に申しわけございません。
で、いまいち良くわからないのですが、構成に関してはともかく、排中律はとても自然に見えるし、さらに便利だと思うのですが、やはりだめなんでしょうか(笑)。あっ、便利というのも一つの徳ということで。
私自身は、最初に経験した数学がブルバキであり、さらに相当真剣に読んだという影響は極めて大きいせいか、その辺り、超越的な概念に違和感が全くありませんし、余り大きい声では言えませんが本当は τ 記号も大好きなのです。便利だから(笑)。もしかして便利さで物事を評価する日和見主義なのかも知れません。
いずれにしても、自分自身に保守的な面や 30年以上前のそれなりスタンダードに対する思い入れがあることは事実かと。
で、もちろん構成的な数学について、良くわからないのは事実なのですが、そもそも分からないことを否定するなどという考えは全くなく、数学という学問は色々広い視点で眺めた方が絶対に良いということを書いたつもりなのが本文の内容なのです。ですが、余り上品でない記述になった部分があるのは恥ずかしい限りです。
外延性の公理については、前に一度 Stromdorfのさんのところで読ませて頂き、あっ、数式抜きなので真面目に読んでなくてほんとに失礼なのですが、驚いた記憶があります。結局良くわからないで放置してしまったのですが、外延性の公理がない集合論は全くイメージがわきません。ただ、対応する消去規則を導入すれば良いとのことと思われますので、何かうまい方法があるのでしょうか。
それから『非構成的な数学が無意味かというと、そうではなくて、構成的な数学の、ある種の「近似理論」として意味があると考えています』とのことですが、正直、非構成的な部分にも (というかその部分にこそ) 数学的な面白さがあると考えています。特に根拠あるわけでなく単なる直感もしくは好みですが。もちろんそのことをもってStromdorfさんとけんかする気はありません。
超フィルターは大好きです。なんといっても、この二年くらいの勉強で一番面白かった、超べきと強制の要の一つですから。私自身はとても具体的な対象としての感覚を持っています。
それでは今後ともよろしくお願い致します。
お返事ありがとうございます。
排中律が自然に見える、とのことですが、確かに対象が有限個しかないような理論では、この推論規則は、“自然”どころか帰納法を使ってちゃんと証明できるくらい“確かな”推論です。ですが、対象が必ずしも有限個とは限らない場合、排中律が成り立つという根拠がありません。
自然だという感覚は、「『どうして実在しない虚数なんか考えるんですか？』『それじゃあ君は実数が実在するとでも思っているのかね』」という問答と同じことで、単に排中律を「使うことに慣れてしまっているというだけのことに過ぎないように思われます。
それからブルバキですが、私もまさにブルバキによって、数学が循環論法に陥らずに一から構築することができることを教えてもらった最も印象に残った本のひとつです。
ところでそのブルバキのτ記号ですが、これは通常ヒルベルトのε記号と呼ばれているもので、この量化記号は、構成主義数学でも受け入れられるほど「根拠がある」論理記号なんですが、ブルバキではこの記号に対して、いわゆるε公理と呼ばれる推論規則である「∀x(P⇔Q) ⇒ εxP=εxQ」を仮定しています。ところがこの推論規則は外延性定理とまったく同様で、一種の等号の導入規則の一種になっているので、等号の消去規則をこの規則の導入にあわせて変更しないと、構成主義の原理に反するからです。
事実、構成主義論理のもとでε公理を仮定すると、排中律が証明できてしまいます。
それから、このような議論で喧嘩する気がないことは私も全く同様ですが、直観主義論理を古典論理より「下に」見ている数学界の意識があることが昔から不満で、論理というものを根拠から構築していくという態度を徹底すると、まず最初に自然に出てくるのは直観主義論理の方であり、これを「二重否定命題を正しいとみなすことにする」という人工的な解釈によって「正しさ」の定義を緩めることによって得られるのが古典論理だ、という（超数学的、シンタクス的な）事実を、数学に携わる人たちにはちゃんと理解してほしいな、とまことに僭越ではあるけれども日々思っている次第なわけです。
Stromdorfさん、あけましておめでとうございます。
私自身は無限領域に対して排中律が不自然とは思っていません。ただし根拠がないと言うことであれば、そのような観点もあり得るし、その方面からの研究が大切であることも分かります。申しわけないのですが、こちらの方面に関して全く無知のため、少々時間がかかるかと思いますが、少しなりとも勉強できましたら、もう一度考え直したいと思います。
τ 記号に関しての等号の消去規則についても一度勉強したいと考えております。
で、直感論理を古典論理より「下」に見ているという風潮に関しては良くわからないのですが、もしそうであればヒルベルトからブルバキへの流れでの、実績ともしかすると権威による影響は大きいのかも知れません。ただし、その流れでの二十世紀数学の成功を見る限り、古典論理が全く見当はずれということはないと思いますし、上下は別として、強い概念なり公理を使用することにより、内容が豊富になるという面は否定出来ないと思います。
正直なところ好きになれないのは、純粋な数学的な観点からではなく、計算機に合わせるために無理矢理数学をゆがめる風潮が見られない訳ではないと感じている部分です。このようなことを言うのは失礼かと存じますが、Stromdorfさんのように、数学の根底の部分に対する深い洞察を行われている方を非常に尊敬しているのはもちろんです。
それでは良いお年をお過ごしください。失礼致します。
Stromdorfさんが私の言いたかったこともよりうまく仰られているので、いくつかコメントにとどめたいと思います。
まず、前回のコメントについて補足させてください。「構成的でない数学は無意味」と書きましたが、これは構成的にはどのようにしても意味を与えれることができない数学、というつもりです。実際には多くの(通常は非構成的に行われている)数学の活動が構成的であることが示せますし、今後研究が進むことで構成的に意味づけられるものもあるでしょうから、これにあてはまる数学の活動はそんなに多くないと考えています。非構成的な数学に基づいた活動も構成的に解釈しなおすことがたいていの場合できますから、その意味で非構成的な数学も意義があるかと思います。
あと付け加えると、構成的に解釈できない数学でも物理などの応用によって、直接意味が与えれる可能性があるという気もしています。この辺りは私もまだ考えを固め切れていません。
かがみさんのその後のコメントについてですが、構成主義は数学とはどのようにあるべきか、という考察の長い歴史の積み重ねから生み出されてきたもので、決して計算機科学に合わせて「数学を歪めた」ものではありません。この点はご理解ください。有限基底定理も、ヒルベルトの定式化は構成版にむしろ近くて、ヒルベルト自身ある種の計算過程として証明を構成しています。ネーター性を使った現代的な定式化はそういった部分を捨象した上で一般化を行っています。それを美しいと思うかは人それぞれだと思いますが、構成版に比べて情報が落ちているのですね。情報を落とした上で一般化をするのは構わないと思いますが、より詳しい定理もあってよいと思います。
あともう一言だけ。数学的に美しいとか、醜いとか言われるのはたいてい慣れの問題です。私にはネーター環とか使わないほうの基底定理のほうがずっと美しく見えます。
yoriyukiさん、明けましておめでとうございます。コメントありがとうございます。今まで色々お話を伺い、私自信の考えに偏った面も多々あることを教えて頂いたと思います。確かに若い頃接した文化の影響はかなり大きいようで、かなり固執している面はあるかと。主観的な面もある「美しさ」に対する感覚も、多様に認めることが大切であり、生産的であることも教えて頂きました。
そうは言うものの私の数学の基盤はやはりブルバキにあるようで、そのような観点から思考することは変わらないと思います。ただ、多様な考えを聞き知ることは、今の勉強にもプラスになると思いますので、今後とも色々教えて頂けるとうれしいです。
それでは良いお年をお過ごしください。
>ブルバキについて
ブルバキは読んだことがないのです。とはいえ、数学上の構造主義といわれるものは気になる存在ではあって、読まなくてはと思っています。私が読んだり話を聞いたりした範囲では(例えば「数学セミナー」にのる一般向けの話)では、ブルバキは最近ではかなり否定的に語られることが多いようですが、少なくとも(informalとは言え)一定の観点から数学を整理したという功績は認められるべきだと思います。
で、ブルバキをきちんと読まないのにコメントするのはおかしいとは思うのですが、数学を集合論的に規定された構造を扱う学問だ、という考え自体はそれなりに価値のある考えだと思います。ただ、私は数学の「構造」を規定している「集合」概念を、公理的集合論が与えている一階の構造として規定するのはあまり説得力を感じません。もちろん、それらの「近似」として公理的集合論を研究することには十分意味があるとは思います。個人的な意見ですが、数学で直観的に扱われている集合概念としてはMartin LeofのIntuitionistic type theoryが一番美しい(かつ哲学的な正当化が示されている)と思っています。もっとも、おそらくいろいろな公理的集合論と等価性が示される可能性が十分あるとも思っていますが。
どうも自論(しかも未整理な)を長々と語りすぎたようです。数学の基礎(｢数学の哲学｣と呼ぶべきだと思っていますが)については、議論しないのが数学として正しいあり方、という雰囲気を(基礎論研究者に)感じてしまっていて、それはそれで不毛ではないかと思いがかがみさんに向かってしまったようです。(とりあえず面倒な哲学的論争には関わらずに数学をやった方が当座の戦略としては有効、という場合が多いのは事実だと思いますが、人間の知的活動に線を引いてそれを越えることを禁じるかのような態度は、学問の進歩を妨げるものだと思います。)やや感情的な言い方になったことをお詫びします。
それから申し遅れましたが、あけましておめでとうございます。
新年明けましておめでとうございます。
もうこれ以上議論するのもヤボかなあと思ってたんですが、yoriyukiさんもコメントを書いておられるので私も悪乗りして（笑）。
yoriyukiさんがMartin LeofのIntuitionistic type theoryについて言及されていますが、この外に、直観主義論理自身の正当化としてはCurry-Howard対応が言及されることが多いと思います。
しかし、ここからは私見ですが、直観主義論理とか構成主義数学というのは、もっと根源的な、もっと初等的なところで正当化されるような気がしていて、今回の私のページのURL（構成主義数学における集合論の正当化）のように、１階の述語論理では（命題変数という概念がないので）変数で表すことができない「命題（ブルバキの言う関係式）」を「項（ブルバキの言う対象式）」に“翻訳”してしまうというテクニックが要するに「集合」という概念なのだと思います。つまり、集合が“モノの集まり”だというイメージは、世俗世界からの類推に過ぎず、そのようにイメージする方が考えやすい、というだけであって、集合概念の本質は、このような「２階の論理を１階の論理の中で扱うための単なる方便」以上の何物でもないと個人的には思っています（私のURLでは、この理論拡大を“冪理論”と名付けています）。
ではブルバキなども依拠しているZFCとかの公理的集合論は何なんだ、ということになりますが、これは更に冪集合とか非順序対とかの存在公理を持つわけで、これに対応する構成主義数学の概念をMartin LeofはIntuitionistic type theoryとして定式化したわけですが、この本質は、上で述べた「冪理論」を取るという操作を再帰的に繰り返していった結果ということを定式化したものと言えると思います。
つまり、最初に与えられた理論の（私のURLで言うところの）冪理論は、それで一つの理論ですから、これの冪理論を作ることができ、さらにそれの冪理論を作る、ということを好きなだけ繰り返すことができますが、理論を展開している最中に、議論の土台となっている理論を拡大するというのは面倒なので、最初からこのような理論拡大が、再帰的に、当該理論の中で行えると便利なので、そのようなカラクリを定式化したものが私のURLで言う「再帰的集合論」なわけです。
ちなみにMartin Leofのtype theoryでは「自然数」を天与のものとしていますが、「再帰的集合論」の考え方を使うと、自然数の構築や、更には無限公理なども、天与とせず、既存の概念から構築することができます（私のURLの第10節の「自然数」参照）。
そして冪集合の公理、非順序対の公理、空集合の公理、分出公理、和集合の公理、無限公理は再帰的集合論で正当化されますが、置換公理と外延性公理だけは正当化できません。そしてBishopの例の本の議論はほとんどこの再帰的集合論における議論だと解釈することができるのです。
おっと、自論をくどくど書いてしまってすいません。また論争口調になってしまっていることを改めてお詫びします。
私は数学に対しては全く創造的な貢献をしてきませんでしたが・・・（ちなみに私は数学科の出身です。私学ですが）
別に「数学は構成的でなければならない」と考えているわけではありません。物事には限度というものがありますから。
ただ、数学における思考を、記号操作に還元してしまったら、それは結局なんでもかんでも算術になっちゃうんじゃないかとかいう、子供じみたことは考えてますが。（このような発想は、数学を高尚なものだと考えたがる人には、低俗に見えるでしょうが、私はむしろ「算術はユニバーサルだ」と思っているので、決して低俗化というつもりではないことを申し添えておきます。）
ああ、それから古典論理を否定するつもりも毛頭ありませんが、例えば線形論理とかなんていうのを知ると、「ああ、古典論理どころか、直観主義論理ですら、まだまだ論理の全体からするとホンの一部なんだなあ。論理の可能性は無限だよ」などとオメデタイことを思ってしまいます。
ああ、そうそう、Curry-Howard対応の話が出てましたが、あれは別に直観主義論理だけに通用する話ではなくて、他にもいろいろな論理の解釈に使えるようですね。
最近、私は論理における資源問題に目覚めてしまいましてcontractionをジャカスカ使うのは環境にやさしくないのではないかとかしょうもないことを考える日々でございます。
通りすがりさん、コメントありがとうございます。
全然反応になっていませんが、今回の事柄に関し、2007年1月19日の記事に、ちっともまとまらないまとめを書きました。