カテゴリー: proof theory

米田の補題（Yoneda Lemma）と反射原理（Reflection Principle）の同型性についての定義。米田の補題（Yoneda Lemma）と反射原理（Reflection Principle）の間に見出さ…
Read more

境界の外側からの証明と境界の内側からの証明はいずれも同値となるということではないか。つまり、宇宙開発をすることなく、地球文明の情報保存は大気圏の内側の情報だけで完全に可能である。 米田の補題（外部との関係性による定義）と…
Read more

コホモロジー（Cohomology）は、トポロジー（位相幾何学）において、空間の「穴」や「構造」を代数的な道具（群や環）を使って測るための手法です。ホモロジー（Homology）の共形のような存在ですが、現代数学ではコホ…
Read more

伝統的なEqualityはより等号の条件を緩和した一般的なEquivalenceの部分集合である。 Homotopical Equality≠Classical Mathematical Equalityであるので、この…
Read more

Teleological Finity Bypassing とは、特定の**「目的（Telos）」を最終的な「同一性（Identity）」としてInvariants化し、そこに至るまでの膨大な「有限のステップ（Finit…
Read more

証明アシスタントとライブラリの対応表 証明アシスタント (Tool / Language) 主要な数学ライブラリ (Library) 特徴 Coq UniMath / Mathematical Components Un…
Read more

Coq（現在のRocq）の歴史は、ChatGPTやGeminiといった現代の生成AIが登場するよりも遥かに長く、深いものです。 1. Coq Coqの開発が始まったのは1984年。フランスのINRIA（国立情報学自動制御…
Read more

UniMath 通常の数学者が紙とペンで書く「定理と証明」が、Coqの世界ではどのように「型（Type）」と「項（Term）」に置き換わるのか。 1. 「証明」という名のプログラム コードは関数型プログラミング（Hask…
Read more

ウラジーミル・ヴォエヴォドスキー（Vladimir Voevodsky）の業績、「代数的K-理論・モチヴィック・コホモロジー」「ホモトピー型理論（HoTT）・単価基礎（Univalent Foundations）」 ウラ…
Read more

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