カテゴリー: Proof Theory

Higher Inductive Types (HITs) の日本語での定義は、ホモトピー型理論（HoTT）における「型の新しい構成法」として次のように記述されます。 従来の型（データ型）の定義が「値（点）」のみに注目し…
Read more

「Truncatability（切断可能性）」は、高次カテゴリー論やホモトピー理論において非常に専門的な意味を持つ概念です。 一言で言えば、「高次の複雑な構造を、低次のデータだけで完全に復元できるか？」という性質を指しま…
Read more

子供の頃からの疑問がやっと解決できた。私は文法、文脈、論理というほとんどの人が信じているものを幼い頃から認知することができていない。論理や文法、あるいは隠喩や暗黙のルールで感動することができないのである。その理由がやっと…
Read more

「境界の境界はゼロである」という直感が、d2= 0 という簡潔な数式に凝縮されるまでには、人類の数千年にわたる「形」と「数」の格闘がありました。 この歴史は、バラバラだった幾何学（目に見える形）と代数（計算のルール）が、…
Read more

ケヴィン・バザード（Kevin Buzzard）とLean（リーン）の登場は、数学界における「ボエボドスキー以降」の最も熱いムーブメントです。ボエボドスキーが「理論的基礎（OS）」を作ったとすれば、バザードはそれを「実用…
Read more

Vladimir Voevodskyウラディミルボエボドスキーがフィールズ賞を受賞する決め手となった「モティーフ・コホモロジー（Motivic Cohomology）」は、代数幾何学における「統一理論」への挑戦です。 「…
Read more

数学は計算技術として始まり、のちに計算を省略する技術として発展しました。人類の「認識の解像度」が上がるにつれて、宇宙の記述形式、および、宇宙の外の記述形式（Axiomaticity）がより抽象的かつ普遍的な階層へとシフト…
Read more

マルティン＝レーフの再帰定理 (Martin-Löf’s Recursion Theorem) は、計算理論（計算可能関数論）における極めて強力な「自己言及の保証」です。「自己言及命題が真であること」を、数学…
Read more

一価性公理（Univalence Axiom）は、数千年にわたる「等しさとは何か？」という問いに対する、数学の地殻変動の終着点です。 古代の幾何学的直感から、近代の論理的厳密性、そして現代の計算機科学へと至る、「公理（A…
Read more

「自己言及命題が真（あるいは無矛盾な体系内での正当性）であること」を巡る、数学・論理学・計算機科学の歴史的な理論一覧。これらの理論は、単なる「言葉遊び」としての自己言及を、「計算可能な再帰」や「自己複製するシステム」、さ…
Read more