「数学基礎論三つの神話」は、1998年に logic-ml メーリングリスト上で行ったアンケートを元に書いた、数学セミナー1999年６月号の記事です。記事の中で、このホームページの広告をしたので、それでこのホームページにきてくださった方もいると思います。
以下に、そのアンケートと、その”解答”を置きます。アンケートの解答というのは妙なのですが、このアンケートは、この事実は正しいと思っていたかどうか、という形式だったので、事実はどうだったかの説明を解答としたのです。
数学セミナー７月号がでたら、６月号の「数学基礎論三つの神話」をそのままここに載せますが、それまで待たずに、是非、数学セミナーを買いましょう。（＾＾）
６月１３日追加： 数学セミナー６月号発行から１ヶ月たちましたので、記事を掲載します。
数学セミナーの威力か、おかげさまで、凄い反響です。Ｖ（＾＾）
まだ、次の号がでてませんので、日本評論社との約束で、記事を載せられませんが、記事に著書がでて来た一松先生からも、お葉書をいただきました。恐縮です！
一松先生のお勧めもあり、次の数学会の基礎論と歴史の分科会で、この関係の話しをしようと思っております。でも、最近、数学会に行かなくなったので、いつあるか良くわからないのですよね。（＾＾；）
それから東京農工大の前田先生から、記事の誤りをご指摘いただきました。（どこまでも、粗忽な林です・・・）。
記事では、ヒルベルトの第２問題を、Die Widerspruchfreiheit der arithmetische Axiome と書きましたが、正しくは、Die
Widerspruchlosigkeit der arithmetischen Axiome です。実は、忙しかったので、記憶に頼って書いてしまったのです。（＾＾；）
それから、タルスキがゲーデルの論文からの影響を書いた部分は、英訳に際しての追加であるように書きましたが、これはドイツ語版にすでにあるようです。直接、原著を見ての確認は、とれておりませんが、前田先生に見て頂いたところでは、まず、間違いなさそうです。これも合わせて訂正します。考えてみれば、ドイツ語版に経緯を書いてなければ、タルスキが非難されてもしょうがないことになりますね。それを考えれば、わかりそうなものを。実は最後のノートが historical note となっていたので、何となく後で付け加えたような印象を持ってしまったのです。お恥ずかしい。
ただ、以上、２点の変更は、数セミの私の文章の論旨には影響を与えませんので、申し添えておきます。
前田先生からのメッセージは、実に有益でした。どうもありがとうございました。
logic-ml のみなさま
林晋＠工学部.神戸大学です。
最近、ようやくこのリストに入れてもらいました。
どうかよろしく。
さて、本題です。
この数年、数学基礎論と論理学の歴史を調べておりますが、常識と思って長年
信じていた``歴史的事実''が間違っており驚くことが何度かありました。いろ
いろな方に尋ねてみると若い方にも同じような間違いをしている方が結構いらっ
しゃいました。どうも、私だけが特別に粗忽なわけでもなさそうです。
それで、どれくらいの数の＊専門家＊が誤解されているものか興味がわいてき
ました。そこで logic-ml でアンケート(？)をとらせていただこうと思い立ち
このメッセージを書いている次第です。
以下に``常識''として流通していると思われるもので、誤りであるものをリスト
しますので、それぞれの歴史的事実を、ご自分はどのように認識されていたかお
教えくだされば大変幸いです。(実はすべて私自身が誤解していたもので、
なかには一般向けの本にそう書いてしまったものせえあります。(^^;) )
``正解''は別のメッセージでお送りします。もちろん、``正解''が実は間違って
いるかもしれません。おかしいことを書いておりましたらご指摘ください。
アンケートの回答は、
shayashi@kobe-u.ac.jp
にお送りくだされば幸いです。
一応、締め切りは無しで、適当に数が集まりましたら集計します。
また、集計結果は、この ml に報告いたします。
アンケートに御協力いただいた方のお名前はご本人の許可がない限りだしません。
では、アンケートです。
++++++++++++++++++++++++++++ アンケート ++++++++++++++++++++++++++++++
以下の設問に (a), (b), (c) でお答えください。
(c) は、一部はそう思っていたが、一部はそう思っていなかったというような場合や、
そんなことは考えてもみなかった、という風な場合に、とにかく、(a), (b) に当ては
まらないときにお選びください。その場合は、ご自分がどのように認識されていたか
お教え頂けると大変幸いです。
また、コメントがある場合は、何でもご自由にお書きください。こんな誤解をするのは、
慌て者のお前だけだ、などという過激なものでも結構です。(^^;)
実際、これらの誤解は海外で出版されている解説書や文献を読んでいれば絶対にしないような
間違いばかりなのですから………
1. Hilbert は彼の有名な``数学の問題''のひとつとして自然数論の無矛盾性をあげた。
(a) そう思っていた。
(b) そう思っていなかった。
(c) その他
2. Tarski は真理概念の定義不可能性定理を、Godel の不完全性定理より早く、
そして、独立に得ていた。
(a) そう思っていた。
(b) そう思っていなかった。
(c) その他
3. Godel は、1931年の有名な不完全性定理の論文で、第1階算術、つまり、我々が
現在 PA とよんでいる第1階の形式的体系、つまり、
第1階の述語論理
等号の公理(と規則)
successor の公理(数学的帰納法を含む): \lnot S(x)=0,....
*, + を定義する公理: x+0=0, x+S(y)=S(x+y),...
の(第1)不完全性を証明した。
(a) そう思っていた。
(b) そう思っていなかった。
(c) その他
4. Godel は彼自身の第2不完全性定理にもかかわらず、Hilbert の有限の立場による
算術あるいは数学(?)の無矛盾性証明の可能性を信じていた。それは1931年の論文
の最後のコメントから明らかである。
(a) そう思っていた。
(b) そう思っていなかった。
(c) その他
+++++++++++++++++++++++++ アンケート終り +++++++++++++++++++++++++++
以上です。どうかよろしくお願いいたします。
林＠神戸大です。
私がお願いしたアンケートの回答の集計、および、私の``正解''を post します。
まず、最初にお断りしておきたいとおもいますが、多くの方から詳しいコメントを
頂きましたが、時間がなくて、十分に分析できておりません。今回は、数の集計
だけで、それぞれのコメントの分析は、またの機会にさせていただきます。
それから、もう一点、私が歴史に興味をもち、調査を続けているのは、幾つか
の出版社から、不完全性定理や数学基礎論についての本を依頼されたからです。
今回のアンケートの結果や、それにともなう議論は(水面下で大部やっております)、
これらの著書を書く際に非常に役立ちそうなので、使わせていただきたい思います。
お許しがない限り、誰々がこんな風に書いていた、などとは、決して書きませんが、
アンケートをとってみたら、やはり、間違いが多かった、という位には書かせて
いただきたいと思っています。アンケートに御協力いただいた方々は、
これをどうか御了承ください。
＃ もし、そんなの止めろ、というご意見がありましたら、ご一報ください。
また、以下の``正解''は、それらの著書のために調査し、考えた結果であり、
著書の下書きのようなものです。ですから、調査結果や、文章を、外でお使い
になるようなことがある場合には、私にご相談ください。
さて、それでは、アンケートの集計結果と私の調査結果です。
--------------------------------------------------------------
アンケート集計結果
結局、１６名の方からご回答をいただきました。
１６名回答者の方々は、論理学(数学基礎論)あるいはその関係分野(理論的計
算機科学など)で研究者として活動されているか、あるいは、以前、活動なさっ
た経験がある方たちばかりです。
``専門家のご意見''と書いたのがたたったのか、学生の方メッセージは１名
(院生、専門、論理学)だけでした。
回答の内訳を表にしますと、次のようになります。
| 問１ 問２ 問３ 問４
----+--------------------
(a) | 7 8 3 7
(b) | 5 4 9 6
(c) | 4 4 4 3
ちなみに、
(a) そう思っていた。
(b) そう思っていなかった。
(c) その他
であり、問１〜４は、つぎのものでした；
問1. Hilbert は彼の有名な``数学の問題''のひとつとして自然数論の無矛盾
性をあげた。
問2. Tarski は真理概念の定義不可能性定理を、Godel の不完全性定理より早く、
そして、独立に得ていた。
問3. Godel は、1931年の有名な不完全性定理の論文で、第1階算術、つまり、我々が
現在 PA とよんでいる第1階の形式的体系、つまり、
第1階の述語論理
等号の公理(と規則)
successor の公理(数学的帰納法を含む): \lnot S(x)=0,....
*, + を定義する公理: x+0=0, x+S(y)=S(x+y),...
の(第1)不完全性を証明した。
問4. Godel は彼自身の第2不完全性定理にもかかわらず、Hilbert の有限の立場による
無矛盾性証明の可能性を信じていた。それは1931年の論文の最後のコメントから
明らかである。
それでは、詳しい解説の前に、まず、``正解''です。
``正解''
| 問１ 問２ 問３ 問４
--+--------------------
| 誤 誤 誤 (誤)
問４にカッコがついているのは、単純に誤りというとちょっと問題があるからです。
実は、問４はみなさんのご意見を聞こうと思って、意識的に曖昧な設問にしました。
ですから、これは正しいとも間違っているとも言いづらい問です。
他の３問は、文献を調べれば正誤がはっきりと判定できる問です。
ちなみに、私はといえば、調べる前は全部間違えておりました。
全部間違えている人は、自分位ではないかと、恐れておりましたが、
少数ですが仲間があり安心しました。(^^)
それでは詳しい解説です。
--------------------------------------------------------------
``正解(？)''の解説
問１から問４まで順に私の調査結果を解説します：
問１. Hilbert は彼の有名な``数学の問題''のひとつとして自然数論の無矛盾
性をあげた。
これは間違いです。
"数学の問題"で Hilbert が提唱したのは、自然数論ではなく実数論の無矛盾性
証明なのです。
第２問題のタイトルは、
Die Widerspruchfreiheit der arithmetische Axiome
なので、``現代的''な言葉づかいですと、``算術の公理の無矛盾性''になって
しまいます。
ところが、Hilbert のこの算術とは実数論の算術なのです。原文(Archiv f. Math.
u. Phys. 3. Reihe, Bd. 1. S.44-63;S.213-237, 1901)は、
Die Axiome der Arithmetik sind im wesentlichen nichts anderes als die
bekannten Rechnungsgesetze mit Hinzunahme des Axioms der Stetigkeit.
です。和訳は、
(その)算術の公理とは、周知の計算規則に連続性の公理を追加したものの
他ならない
となります。
岩波数学辞典では、``算術の無矛盾性''になっております。間違いとまでは言え
ませんが誤解を招きます。これを読んで私は長らく first order arithmetic
のことだろうと信じていました。(T_T)
一松信先生のヒルベルトの問題の古い和訳(共立)では、im wesentlichen
nichts anderes als die が誤訳されて、連続性の公理以外のもの、という意
味になっており、解説にも Gentzen などが引用されて PA の無矛盾性である
かのように書いてあるものがあります。多分、それ後の版では修正されたの
ではないかと期待しますが、一松先生でも間違うというトリッキーな題名です。
ようするに、arithmetische という言葉の使い方が日本語の算術とえらく違う
のですね。
問２. Tarski は真理概念の定義不可能性定理を、Godel の不完全性定理より早く、
そして、独立に得ていた。
``早ければ独立だろう''というコメントをいただきました。いや、
ごもっとも。(^^;)
さて、本題にもどります。
これは間違いです。決定的な証拠もあります。
Tarski 本人が詳しい経緯を書いているのです。
これが一番誤解率が高く。16名中半分の8名の方が、Tarski の定義不可能性定理が、
先だと信じておられました。そうではないと思っていた方は、その半分の4名です。
では、詳しい内容です。
``普通の誤解''(?)では、Tarski の結果は Poland 語で、Godel の論文より早く
発表されいた、となっています。これは事実です。しかし、それには、
定義不可能性定理は無かったのです。
Tarski の論文集 Logic, Semantics, Metamathematics, Oxford at the
Clarendon Press, 1969, の Tarski の真理概念の論文の英訳
The concept of truth in formalized languages
の p.154, p. 247, p.277-8 に付けられた Tarski 自身による大変悔しそうな
脚注によりますと、n+1 order の論理による n orderの論理の真理概念の定義
可能性は Godel 以前に得られており、それが 1929 年に得られ、1930年には
講義の形でポーランドで発表されているが、同じ階数では定義不可能となると
いう定義不可能性定理とその証明は、Godel の 1931年の論文を見た後で追加さ
れたという事情がわかります。
ただし、Godel と同じような感触は持っていたようで、p.247 の脚注に、それ
が見えます。しかし、定義不可能性定理の証明法は、Godel の方法によると
はっきりと明言されています：
p.247 脚注
We owe the method used here to Godel, who has employed it for other purposes
in his recently published work,
Godel, K. (22: これが1931年の不完全性定理論文),...
この文章は冷静ですが、他の文章は、(下手なわかりにくい英語で)、悔しそう
に、かつ、自分の理論が Godel の定理とは違うのだと必死に強調して書いてあり、
悪趣味ですが、偉い人の四苦八苦を見物してよろこぶには最適です。(^^;)
ただし、Tarski の名誉のために一言付け加えておきますと、Tarski は、
Godel の定理にケチをつけるようなことは一切しておらず。Godel の論文を
This exceedingly important and interesting article
と讃えています。
私は Tarski が先だと20年以上信じておりましたので、これを見付けたときに
は大変驚きました。
おはずかしい話ですが、小著``ゲーデルの謎を解く''(岩波書店)にも、この間
違いがあります(p.103)。 岩波の編集部との連絡の手違いのため数ヵ月前にで
た最新の第6刷でも訂正できておりません。次の刷で訂正いたします。読者の方
にはこの場をかりて平にお詫びいたします。(m0m)
この間違いは日本だけのことのようで、海外の通俗書などみましたが、同じ間
違いは見付けることができませんでした。
自分が何でそう思うようになったか、あまりに昔のことで思い出せないのですが、
昔読んだ本などひっくりかえしてみますと、竹内外史先生のロジシャン小伝のタ
ルスキーの項に
上述の論文はゲーデルの論文のあとで出版されたのでゲーデルの亜流という
批評が一時あったが、じつは彼はもともと論文をゲーデルより先にポーランド語
で書いていて、右の論文はその翻訳なのである。
(初出: 数学セミナー 1969, 4〜6, 竹内外史著、``現代集合論入門''と
``ゲーデル'', ともに日本評論社, に収録)
とあります。上述の論文というのが、The concept of ... です。まさに竹内先生が
書かれたその通りで間違いではないのですが、定義不可能性定理が Godel の論文を
見たあとで付け加えられたという経緯が書いてないので、これでは読者は間違えて
しまいます。
同じ間違いは、広瀬健・横田一正両先生の``ゲーデルの世界''(私が持っているのは
第7刷)にもあります。ここでは、Godel の先行性に対して Tarski が
「ゲーデルより完全でそれとは独立なものだ」といっている
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
とありますが、これは Tarski が前述の脚注 p. 278 で
<<自分の論文の結果のひとつは>> the discussions on pp. 184 f. on the
interpretation of the metasystem in arithmetic, which already
contain the so-called `method of arithmetizing the metalanguage'
which was
developed far more completely and quite independently by Godel.
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
と書いているのを誤解されたのではないかと思います。"by Godel" ですから、
Godel の方が、遥かに完全でまったく独立にやった、と言っているのです。
ちなみに、`method of arithmetizing the metalanguage' とは、メタ理論の
ゲーデル数による算術化のことです。Tarski は Godel と違って explicit に
形式言語の coding をあたえることはせず、formal language の expression と
natural numbers に 1 to 1 がつくことはあたり前だとして議論を進めて
います。Tarski の目的は(natural number を前提として)強い論理で一つ下の
論理の interpretation を与えることだったので、それで十分だったのです。
一方、Godel は、undecidable proposition を算術的に表せることを証明する
ために、Godel numbering のような詳細な coding を必要としたわけです。
問３. Godel は、1931年の有名な不完全性定理の論文で、第1階算術、つまり、我々が
現在 PA とよんでいる第1階の形式的体系、つまり、
第1階の述語論理
等号の公理(と規則)
successor の公理(数学的帰納法を含む): \lnot S(x)=0,....
*, + を定義する公理: x+0=0, x+S(y)=S(x+y),...
の(第1)不完全性を証明した。
さすがに、これが最高(9/16)の正答率でした。
多くの回答者の方たちのご指摘のとおり、Godel が1931年の有名な不完全の論文
Uber formal unentscheidbare Satze der Principia Mathematica
und verwandter Systeme
で実際に証明したのは、そのタイトルどおり、"Principia Mathematica と
それに関連する体系"の第1不完全性 Satz IV だけです。
(もちろん、仮定はω-無矛盾性です。)
私はこれを ``PA の不完全性も示した'' と誤解しておりました。
その理由は、Part 3 において、中国剰余定理を使った非決定性命題の
arithmetization の議論がなされているからです。つまり、Godel は、
Part 3 において、PA の論理式で表現できる Principia Mathematica の
決定不可能命題を作ってみせているのです。
それで私は短絡して、Godel の証明は PA に直接適用できる、と誤解して
いたのです。最近、この 1931 年の論文を完全に和訳する機会があり、
改めて読み直して、自分の間違いに気がつきました。
＃ところで、この和訳を読んで批判をしていただける方はいらっしゃい
＃ませんでしょうか。これについては、logic-ml にすぐに別のメッセージ
＃を送ってお願をいたします。
つまり、Godel は、1931年の論文で、不完全性定理の証明に必要な関数、
つまり、primitive recursive function は、すべて PA の論理式で
定義可能であることを証明しているのです。
しかしながら、その証明には、primitive recursive function が使われて
います！つまり、現代的なやり方では、primitive recursive function の
定義をみたす関数のグラフが PA で定義できることを示すところを、
最初に primitive recursive function を仮定し、それに同値なグラフ
を定義しているというわけです。
もちろん、ちょっとした technique を使えば、PA の中で、直接に
primitive recursive function の定義可能性をいえるのは、
みなさんご存知のとおりです。
では誰が最初にそう注意したか、つまり、PA で第1,2不完全性定理が証明
できるのを誰が最初に指摘したかとなりますと、まだ、私にはわかりません。
不完全性についての technical paper としては、Godel は 1931年の論文の他
に、1934年に
On undecidable propositions of formal mathematical systems,
Collected Works I, p.346
という論文を書いています(正確には Kleene たちが筆記したIAS での講義録
です。また、講演用のノートならば他にもあります)。
この中で使われているシステムも second order で、しかも、full comprehension
つきです。これは妙なことで、解説を書いている Kleene も、わざわざ、
arithmetical comprehension without function parameters で十分である
ことを、Godel は知っていたのかもしれないが、書いてはいない
と注意しています(CW I, p.339)。
では、誰がどこで、最初に PA の不完全性定理を考えてのか、という疑問がわき
ますが、残念ながら、これがまだ分かりません。
現在の教科書や解説書では、不完全性定理を示す形式系として、大抵、PA が
使われることからすると、何とも気持の悪いことです。
誰が最初か、どこにあるか、どなたか、ご存知ではないでしょうか？
問４. Godel は彼自身の第2不完全性定理にもかかわらず、Hilbert の有限の立場による
無矛盾性証明の可能性を信じていた。それは1931年の論文の最後のコメントから
明らかである。
これは、わざと答えにくくした設問です。つまり、できるだけ、ご意見をいただく
ための、簡単に答えられない設問です。
ですから、``正解''もあってないようなものです。しかし、ご回答のなかから、
一番事実に近いものを選ぶならば、次の二つかと思います：
>Godel がこのコメントで言おうとしたのは、「問題としている形式理論の言語
>で表せないような証明なら、有限的なものが存在しないとは言い切れないから、
>第2不完全性定理が示されたからと言って、ヒルベルトのviewpoint に反する
>とまで直ちに結論づけるのは言い過ぎだろう」ぐらいの事だったのではないか
>と私は思っています。有限的な無矛盾性証明の存在を積極的に信じていたよう
>には私には読めません。
>#「その可能性を否定するものではない」という意味の文章はあったように
>#思いますが、「可能性を信じていた」と思える表現があった記憶がないです。
この設問をお聞きした理由は、この Godel のコメントを引用して、
不完全性定理を発見した Godel 自身が、Hilbert計画の可能性を
否定していない。これにみられるように、それはまだ可能なので
あって、この問題はいまだに大問題として研究が進められている
という印象を受ける議論が解説書に良くみられるからです。
私は、これは現代の研究者の感覚から大きく外れていると思っています。
最近では、広大の新井先生や、ドイツ学派の大変重要な研究が進行中ですが、
これは、Hilbert計画の枠組の中の無矛盾性証明ではなく、数学(数理論理学)
の重要な一分野として研究されていると理解しております。(以前、新井先生
とお話ししたおりには、そのようなお聞きしました。)
また、逆数学にみられる無矛盾性証明も、数学の定理の論理的強さを同定する
ためであり、たまたま、それが有限の立場に hit したときは、本来の
Hilbert計画が成功するわけで、Simpson や東北大の田中先生が強調される
ように、partail fuillfilment であり、Hilbert が本来企画した基礎の問題
に一挙に決着をつけるものではないわけです。
つまり、私が言いたいのは、無矛盾性証明を、Hilbert と同じ動機で行ってい
る人は、現在では、実質ゼロであろうということです。
Godel は、この現代の傾向とは反対の考えをもっていたかどうか？ということ
を問うのが、問４の真意です。
もちろん、この設問の答は有限の立場とは何か、という哲学的問題とかかわり、
さらに、Godel が 1930年当時、それをどう思っていたか、そして、それは以後
どのように変わったのか、という歴史的問題がかかわります。
私が Collected Works や Dawson の Logical Dilemma を読んで得た印象は、
次のとおりです：
Ｇ１. Godel は、1930年には、Hilbert の有限の立場とは何か、また、その証明
が Principia Mathematica で必ず formalize できる、という確信をもって
いなかった。そのために不完全性定理の論文に慎重なコメントを書いた。
Ｇ２. しかし、遅くとも 1933年までには、その意見は大きくかわり、Hilbert計画
は不可能である、と考えるようになる。また、第１、２不完全性定理により
Hilbert計画の epistemological な意味はほとんど無くなってしまった、と
いう意見を表明するようになる。
同時に、哲学的な意味を離れると、より evident なものに数学を還元する
ということは、それ自体が数学的に重要な問題であるとし、Gentzen や
Herbrand の無矛盾性証明を、そのような仕事として高く評価する。
Ｇ３. そして、この姿勢が、おそらく終生つづいた。
また、ついでにいいますと、Godel は、第１不完全性定理を証明する前から、
不完全性定理らしきことを想定していた形跡があり、それを論拠にして、
第１不完全性により、Hilbert計画の意味が、かなりそこなわれることを
主張しています。また、不完全性定理を証明した後も、第１不完全性(第２で
はありません！)により、Hilbert計画の無矛盾性証明の意味がそこなわれる
ことを、繰り返し主張しています。(たとえば、小著、「ゲーデルの謎を解く」
の「控え目な登場」に書きました、ケーニヒスベルクでのゲーデルの発言)。
＃これは北大の辻下先生の投稿と関係します。
＃長くなりますので、ここには書きませんが、そのうち詳しい話を post します。
Ｇ１-Ｇ３の根拠:
Ｇ１の根拠は、Dawson の Logical Dilemma です。p.99 に 1931年の発表のす
ぐ後には, Herbrand や Schlick に対して, Godel は, 有限の立場の議論が必
ず形式化できるどうかには決着が付いていないという, 慎重な意見を伝えてる
そうです。
私は Herbrand や Schlick が Godel に何をいったかは知りませんが、Godel
との通信をみますと、von Neumann も Herbrand たちと同意見だったようです。
そういうまわりの過激な意見(?)にも因われず、おそらく、Godel は 1930年から
1933年にかけて沢山の思考実験を繰り返して、有限の立場が classical
arithmetic の中でさえ形式化されるとの確信を深めたのでしょう。
そういう思考実験なしには、第2不完全性定理が Hilbert 計画の不可能性を証
明するといったところで飛躍がすぎるわけですから。
＃ 話がそれますが、これについて野崎昭弘先生から、``専門家はそういう数学
＃ 以外の部分の分析を説明しないで、Hilbert 計画の不可能性にジャンプして
＃ 説明してしまっているのではないか。だから論拠が弱く誤解が生じるのだ''
＃ と痛いご指摘を受けたことがあります。実にもっともな指摘かと思います。
Ｇ２ の Hilbert計画の不可能性の部分の根拠は、1933年12月の AMS の集会での
invited talk の下書きです(Collected Works III, pp. 45-53)。ここで、
Hilert の有限の立場で無矛盾性証明を行うことは不可能とほぼ断定していま
す: 同論文 pp.51-52
This method possesses a particularly high degree of evidence, and
therefore it would be the most desirble thing if the freedom from
contradiction of ordinary non-constructive mathematics could be proved
by methods allowable in this system A. And, as a matter of fact, all
the attempts for a proof for freedom from contradiction undertaken by
Hilbert and his disciples tried to accomplish exactly that. But
unfortunately the hope of succeeding along these lines has
vanished entirely in view of some recently discovered facts.
中略
So it seems that not even classical arithmetic (これは自然数論です)
can be proved to be non-contradictory by the methods of the system A,
because this proof, if complying with the rules of the system A, would
be expressible in classical arithmetic itself, which is impossible.
Sytem A というのは, Hilbert たちが有限の立場として使っていたものだと
Godel がいっている体系で、あまり、はっきりとは書いてありませんが、
quantifier free primitive recursive arithmetic のようです。
また, Collected Works IIIの講義ノート 1938a には, 無矛盾性証明一般の意
義や, Gentzen の証明に対する Godel の態度が非常に明瞭に述べてあります。
その論点は、
(A) 不完全性定理により、無矛盾性証明の epistemological significance は
very much diminished であるが
(B) 不完全性定理によっても無矛盾性証明の mathematical significance は
totally unaffected である
という態度が非常に明瞭に表明されています。
これは我々の現代の常識にほとんどピタリと合うと思うのですが、
みなさんいかがお考えでしょうか？
この議論が始まると、logic-ml が fj.math になってしまうような危険性を
感じますが……… (^^;)
まとめると、Godel は、無矛盾性証明の意味を二つに明確に分けていたという
ことです。だから、Hilbert計画を否定しながら、Gentzen や竹内先生の仕事を
評価し、また、自分も functional interpretation による無矛盾性証明を考え
たのでしょう。
しかし、(B) の無矛盾性証明を単純に Hilbert計画と呼んでしまうのはどうか
と思います。
Friedman-Sieg の WKL_0 が PRA (quntfier free 版)の保存拡大となるという
結果は、(B) の大変良い例だと思います。
逆数学では、これと WKL_0 の実際的強さをあわせて、``Hilbert 計画の
partial fulfillment''というわけですが、この場合には、``Hilbert 計画''
という用語が conservative extension の言葉で正確に定義されなおします。
そして、それが Godel の (B)のある一つの定式化になっているわけです。
つまり、``逆数学の Hilbert 計画''を定義しなおしているのですから、すっ
きりしていて問題はありません。やはり、逆数学の場合にように、言葉をハッ
キリさせるべきですよね？
Ｇ３. 実は、これには強い論拠はありません。(^^;)
Collected Works I-III を見る範囲では、大きな変化がみられない、
というだけです。たとえば、1951年の有名な Gibbs lecture の論点は、
1933年ころのものと同じです。Collected Works IV で未刊の手紙類が
出版される予定ですが、これを開けてみたら、ビックリということも
あり得ますが、すでに Dawson は、一応目を通しているはずですから、
あまりありそうな話ではありません。
------------------
随分長くなりましたが、以上です。
みなさんのご意見を頂ければ大変幸いです。