ハクソク

世界を動かす技術を、日本語で。

「プリンキピア・マテマティカ」は現代的で洞察に満ちている

2026年8月13日原文(okmij.org)

概要

  • Principia Mathematica は現代のプログラミング言語理論にも通じる先見性を持つ書籍
  • 参照透過性 や 外延性、 型 などの現代的概念を初めて本格的に論じた
  • ラムダ計算 や 直観主義 への先駆的な洞察を含む
  • 定義 や 記号論 への独自の視点
  • 第1章の内容を中心に、現代との関連性を解説

Principia Mathematicaの現代性と先見性

  • 1910年出版の Principia Mathematica は、現代のプログラミング言語理論の文脈でも新鮮さを感じさせる内容
  • 外延性/内包性、 参照透過性、 型 などの概念を詳細に議論
  • domain（定義域）、 アルファ変換、 type（型） などの現代的用語の初出例
  • 不完全記号 という概念は、後の継続や制御演算子の先取り
  • 自由変数・束縛変数・代入・抽象・適用 の概念が言語学に由来することを指摘

参照透過性と外延性

  • p8で 参照透過性 （referential transparency）を初めて明確に説明
    • f(p)≡f(q) ならば p≡q で f(p)≡f(q)
    • A believes p の例で非参照透過的文脈も紹介
  • 数学は常に 外延 （extension）に注目し、 内包 （intension）は重視しないと述べる

定義：記号的便宜とその重要性

  • p12で、 定義は理論的には単なる記号的便宜 と位置づけ
  • しかし、 定義が意図や重要性を示し、共通概念の分析を含む ため、実際には非常に重要
  • 定義の選択＝主題の選択と価値判断

命題関数とラムダ計算の先取り

  • p15で「 命題関数」を導入、これは現代の ラムダ項 に相当
    • 例：「x is hurt」はxが決まらない限り命題ではない
    • \hat{x} is hurt のような記法を導入
    • 自由変数・束縛変数・代入・アルファ同値 の明確化
  • p17で 量化式 と 変数のスコープ を説明
    • apparent variable＝現代の束縛変数
    • real variable＝現代の自由変数
    • ∫abφ(x) dx との類比で説明

「任意」と「全て」：直観主義的視点

  • p18-19で現代の スキーマ変数 や スキーマ主張 （⊢ f x）を議論
    • 任意（for any） と 全て（for all） の区別を強調
    • 任意値の主張は、全ての値が真である場合のみ正当化
    • 全称導入（∀-introduction） と 全称除去（∀-elimination） の概念を説明
  • 直観主義 の萌芽を示唆

存在の直観主義的解釈

  • p20で 存在証明 は「具体的な例（witness）」を示すことが唯一の方法と述べる
    • 構成的証明 ＝直観主義・構成主義的立場
    • Brouwer や Kronecker との関連性

型の概念の初出

  • p21で 型 という語を現代的意味で使用
    • φとψが同じ型の引数を取る必要性 を明言
    • 型システム の先取り

集合所属記号の起源

  • p26で 集合所属記号（∈） の由来を説明
    • ギリシャ語の ε（エプシロン） ＝「存在する」を意味
    • x ∈ man は「xは人間である」の意味

記述関数と関数の定義

  • p33で 関数を二項関係の特殊な形 として定式化
    • 任意の二項関係Rから、 R'y＝「xRyが成り立つ唯一のx」 として関数を定義
    • 定義域（domain） の導入
    • 記述関数（descriptive functions） ＝現代の「定義記述（definite descriptions）」
    • Russellの記述理論 に基づく命名

参考文献

Hackerたちの意見

この本を最初から最後まで読めたら、あなたは本当にヒーローだよ。時々、真ん中に大きな論理的エラーを入れて、誰も読まないだろうって思って人をからかうためじゃないかって考えることがある。

└

まさか、アルフレッド・ノース・ホワイトヘッドのサイン入りバグバウンティ小切手を額に入れて飾ってないの？もっと真面目に言うと、確かにこの全体の中には大きな論理的エラーがあって、それはクルト・ゲーデルによってずっと後になって発見されたんだ。

└

印刷所が何かタイプ設定のミスをする可能性ってどれくらいあるんだろうって考えたことがある。私たちの中で、例えば、バグを入れずにAPLの記号で千ページを打てる人はいるのかな？

└

大学の論理学の授業で必読だったよ。セット理論の授業でもオプショナル（つまり必須）だったと思う。数学史や数学哲学のコースでも、だいたい必ず扱われる内容だね。

└

面白いことに、去年のShow HNでLeanでPMを形式化したものがあったよ（https://news.ycombinator.com/item?id=43797256）。そして、Principia Rewriteプロジェクト（https://www.principiarewrite.com）では、元の証明スケッチに対して189の命題論理定理（セクション1-5）をCoqで検証したんだ。

これを始める前に、彼の『数学哲学入門』を読むのもいいかもね： https://en.wikipedia.org/wiki/Introduction_to_Mathematical_P... 読みやすさを考えると、いろんなPDFバージョンも見てみて： https://people.umass.edu/klement/imp/

└

同様に、作品自体はここで入手できるよ： https://people.umass.edu/klement/pom/

└

もっと面白いアプローチが好きなら、ラッセルの旅を描いた「ロジコミックス」をおすすめするよ（ストーリーのために歴史的に正確じゃないところもあるけど）。https://en.wikipedia.org/wiki/Logicomix

ラッセルとホワイトヘッドに頭を悩ませるよりも、ホモトピー型理論（通称HoTTブック）を読むことを勧めるよ。依存型はクールで思考を広げてくれるけど、高次帰納型は本当に思考を変えるレベルだよ。『リトルスキーマー/タイパー』はHoTTに備えるための準備テキストとして使えるかも。機能型プログラミング言語にもっと適用できる利点もあるし、マックレーンの『働く数学者のためのカテゴリー』よりも、ハスケル初心者に勧められることもあるかもね。

└

HoTTを読んでみたんだけど、最初の章の型理論はすごく良かったし、わかりやすかった。でも、2章では完全に迷子になっちゃった。なんでだったか覚えてないけど、たぶんその後修正されたのかも。ユニバレンス公理には興味があるんだ。タイプに対する別のアプローチ、トリアージ計算を使ったものに興味があって、これは「構造主義」よりも「マテリアリスト」な感じ。型は、正規形の（引用された）項の構造によって与えられるんだ（ラムダ計算とは違って、トリアージ計算は引用が簡単）。ユニバレンスは引用に関連している気がしてて、たとえば2つの引用された項が「標準自己解釈者」の下で等しいなら、それらは等しいみたいな。

└

「マックレーンの『働く数学者のためのカテゴリー』よりも、さらにそうかもね（たまにおすすめされるのを見かけるけど…）」 それに関しては、私はこの推薦には反対だよ。その本は不必要に難解なんだ。カテゴリー理論の良いおすすめは知らないけど、それは違うね。

プリンキピアとラッセルの数学の基礎を求める悲劇的な物語に馴染みがない人のために（ネタバレ：基礎はない）、すごく良いグラフィックノベル「ロジコミックス」があるよ。https://en.wikipedia.org/wiki/Logicomix たぶん10年くらい読んでないけど、なんか理由はわからないけど、ずっと考え続けてる本の一つなんだ。

Hacker Newsで議論の続きを見る