HN 日本語サマリー

← 一覧へ戻る
科学・技術

Principia Mathematicaは現代的で洞察に満ちている

Principia Mathematica is modern and insightful (okmij.org)

245 pointsby matt_d131 コメント

要約

1910年に発表されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』が、現代のプログラミング言語に関するテキストのように読めるという分析です。本書は、外延性/内包性、参照透過性、型といった現代的なトピックを深く掘り下げており、ラムダ計算や直観主義の萌芽も見られます。

全文翻訳

前へ 次へ 開始 トップ Principia Mathematicaは現代的で洞察に満ちている 導入 参照透過性、外延性 定義:単なるタイポグラフィ上の便宜だが、最も重要 命題関数:ラムダ計算の先駆け 任意 vs 全て:直観主義の一端 存在についての直観主義的見解 型 集合メンバーシップの起源 記述関数 導入 Principia Mathematicaは、ホワイトヘッドとラッセルによって1910年に出版されました。それにもかかわらず、現代のプログラミング言語に関するテキストのように読めます。私はPrincipiaを非常に魅力的で、手放せないと感じました。 Principiaは、外延性/内包性、参照透過性、型といった現代的なトピックを、深い洞察をもって論じています。現代的な意味での「ドメイン」、「アルファリネージ」、「型」の最初の言及が含まれているかもしれません。その「不完全な記号」――文脈でのみ意味を持つもの――は、継続と制御演算子を先取りしています。自由変数と束縛変数、代入、抽象、適用といった概念がすべて言語学に由来することを洞察深く観察しています。 私はPrincipiaにすでにラムダ計算が含まれていると感じずにはいられませんでした。また、ラッセルとホワイトヘッドは、例えば「任意」と「全て」のために別々の記法を主張する(彼らの理論ではこれらの概念は等価であると認めているにもかかわらず)ことで、直観主義を先取りしていたようにも思えます。 Principia全体は非常に大きいです。この本は、1+1=2を証明するために1000ページを費やしたことで有名だと言われています。序文で強調されているように、証明は、暗黙の前提が使用される可能性を排除するために、極めて詳細に行われています。 Principiaの目標は、非常に基本的な概念のセットを提示し、それらだけが数学全体に十分であることを示すことでした。もしPrincipiaが今日出版されるとしたら、すべての証明は補遺(または定理証明器)に追いやられるでしょう。重要なのは、基本的な概念とそのセットアップであり、そのほとんどは序文と第1章で説明されています。 以下は、Principiaの第1章を読みながら取ったいくつかのメモです。ジャック・カレット氏から非常に親切にいただいたコメントもいくつか含まれています。 バージョン 現在のバージョンは1.3、2026年8月です。 参考文献 Principia Mathematica by Alfred North Whitehead and Bertrand Russell. Cambridge: University Press, 1910- <http://name.umdl.umich.edu/AAT3201.0001.001> (ミシガン大学歴史数学コレクションによる完全スキャンテキスト、多謝) Linsky, Bernard. The Notation in Principia Mathematica. The Stanford Encyclopedia of Philosophy (Summer 2026 Edition), Edward N. Zalta & Uri Nodelman (eds.) <https://plato.stanford.edu/archives/sum2026/entries/pm-notation/> 参照透過性、外延性 Principiaの8ページには、おそらく数学文献で初めて、内包と外延、そして現在「参照透過性」と呼ばれるものについて言及されています。「p≡qならばf(p)≡f(q)となる」とあります。ここでf(p)は、別の命題pを含む命題です。現代的な言葉で言えば、fをコンテキストと呼び、C[]と表記し、p≡qならばC[p]≡C[q]となると言えます。これは参照透過的なコンテキストの一般的な記述です。ページは次に、非参照透過的なコンテキストの例を示しています。「Aはpを信じている」――これは、pが等価な命題に置き換えられたときに意味が変わる命題です。この例は、この概念の起源が言語学、特にフレーゲ(脚注で言及されている)の研究にあることを示唆しています。本書は、「数学は常に内包よりも外延に関心がある」(ここでもフレーゲの用語を借りているが、英語訳である)と述べています。 定義:単なるタイポグラフィ上の便宜だが、最も重要 p12では、定義は単なるタイポグラフィ上の便宜であると述べられています。一方で、定義は最も重要です。なぜなら、それらは意図を示すからです。「…定義は我々の主題の一部ではなく、厳密に言えば、単なるタイポグラフィ上の便宜にすぎない…。定義は理論的には冗長であるにもかかわらず、定義はしばしば、それらが使用される命題に含まれるよりも重要な情報を含んでいることは事実である…。定義の集合は、我々の主題の選択と、何が最も重要であるかについての我々の判断を具体化する。第二に、…定義は一般的な考えの分析を含んでおり、したがって顕著な進歩を表現する可能性がある。」 命題関数:ラムダ計算の先駆け ページ15では、「命題関数」が導入されています。これは現在ラムダ項として知られています。自分で見てみてください。ページ上の実行例から。「xは傷ついている」[曖昧と呼ばれる]は、xが誰であるかが決まるまで、実際には何も主張していません。しかし、xが保持する個別性のため、それは「xは傷ついている」から得られる命題のコレクションからの曖昧な例であり、真偽を問うことができます。著者たちは次にその「命題関数」の記法:「xは傷ついている」を導入します。文脈中に現れる「xは傷ついている」と「yは傷ついている」は区別できるが、「xは傷ついている」と「yは傷ついている」は意味の違いを全く伝えない。」ここに、自由変数、束縛変数、代入、アルファ等価性があります。変数のトピックは、p17で、量化された公式の議論で再び登場します。「(x).φx」記号[現代の記法では∀x.φ(x)]は、一つの明確な命題を表し、「(x).φx」と「(y).φy」が同じ文脈で現れる場合、意味の違いはない。「(x).φx」記号は、∫abφ(x) dxにいくらか類似しており、どちらの場合もその表現はxの関数ではない。「(x).φx」または「(∃x).φx」に出現するxは(ペアノに従って)「見かけの変数」と呼ばれる。ページは次に、変数のスコープの概念を導入します。Principiaが「見かけの変数」と呼ぶものは、現代の用語では束縛変数であり、「実変数」は現在自由変数と呼ばれます。束縛変数とアルファ等価性の例として定積分が示されているのは印象的です。また、ラムダ計算が長い系譜を持っていることも示しています。ライプニッツの洞察力に感心せずにはいられませんでした。 任意 vs 全て:直観主義の一端 p18とp19のPrincipiaは、現在「スキーマ変数」と「スキーマ断言」と呼ばれるもの、つまり⊢ f xの形式のものを扱っています。実変数を含む何かを断言する場合、例えば⊢ x = x のように、我々は任意の値を断言していることになります。見かけの変数を含む何かを断言する場合、例えば⊢ (x).x = x [現代の記法では⊢ ∀ x. x=x] のように、我々は…その命題関数のすべての値を断言していることになります。任意の値を断言できるのは、すべての値が真である場合のみです。なぜなら、そうでなければ、変数の値はまだ決定されていないため、偽の命題を与えるように決定される可能性があるからです。したがって、上記の例では、⊢ x = x があるので、⊢ (x).x = x を推論できます。 著者たちは次に、現在「一般化」、つまり∀導入と呼ばれるものを導入します(20ページでは逆、∀除去、つまりPrincipiaが言うところの「全てに当てはまることは、任意に当てはまる」を紹介しています)。スキーマ公式(任意について)は、Principiaの論理(後に一階述語論理として整理されたもの)における対応する全称量化された公式と等価ですが、著者たちは依然としてこの2つの概念を区別したいと考えています。数学の通常の公式は、そのような[実変数]断言を含んでいます。例えば、sin² x + cos² x = 1 は、この公式の特定の場合を主張するものでも、xのすべての可能な値に対して公式が成り立つことを主張するものでもありませんが、それはこの後者の主張と等価です。それは単に公式が成り立つことを主張し、xを完全に未決定のままにします。そして、xがどのように決定されても合法的にそうできるのです。