自己言及命題が真であることの証明｜Univalence Axiom
「自己言及命題が真（あるいは無矛盾な体系内での正当性）であること」を巡る、数学・論理学・計算機科学の歴史的な理論一覧。これらの理論は、単なる「言葉遊び」としての自己言及を、「計算可能な再帰」や「自己複製するシステム」、さらには「現代数学の新たな基礎」へと昇華させた歩みです。
自己言及命題の正当性と真実性に関する理論一覧
| 年代 | 提唱者 | 理論・概念名 | 内容と「自己言及の真性」における意義 |
| 1931年 | クルト・ゲーデル (Kurt Gödel) | 不完全性定理 / ゲーデル数化 | 「私は証明できない」という自己言及を算術（数）に変換。自己言及が数学の「記述」の中に厳密に存在し得ることを証明した。 |
| 1934年 | ハスケル・カリー (Haskell Curry) | Yコンビネータ (不動点結合子) | 名前を持たない関数が「自己」を呼び出す仕組み。自己言及を「計算の動力（再帰）」として定義した。 |
| 1938年 | スティーヴン・クリーネ (Stephen Kleene) | クリーネの再帰定理 | 任意の計算可能関数において、「自分自身のコードを参照して動作する」プログラムが必ず存在することを証明。自己言及の計算上の実在を保証。 |
| 1940年代 | ジョン・フォン・ノイマン (John von Neumann) | 自己増殖オートマトン理論 | 自分の設計図（自己言及情報）を読み取り、自分を複製する機械の数学モデル。自己言及を「生命現象」として定義。 |
| 1950年代 | ウィラード・V・O・クライン (W.V.O. Quine) | クイン (Quine) / 自己参照文 | 入力なしで「自分自身のソースコード」を出力する論理。自己言及が「出力」として真に実現可能であることを示した。 |
| 1960年代 | グレゴリー・チャイティン (Gregory Chaitin) | アルゴリズム情報理論 (Ω数) | 自己言及的なプログラムの停止確率を定数化。コルモゴロフ複雑性と自己言及を結びつけた。 |
| 1969年 | ウィリアム・ハワード (William Howard) | カリー＝ハワード同型対応 | 「証明」と「プログラム」が同型であるという説。自己言及的な証明が、実行可能なコード（真）として扱える基盤。 |
| 1970年代 | サウル・クリプキ (Saul Kripke) | クリプキの真理理論 | 自己言及を含んでも矛盾しない「真理の階層」を定義。パラドックスを回避しつつ自己言及を「真」として扱う枠組み。 |
| 2006年頃 | ウラジーミル・ヴォエヴォドスキー (Vladimir Voevodsky) | 一価性公理 (Univalence Axiom) | 「同値なものは同一視できる」という公理。自己言及的な型定義を現代数学の「真なる基礎」として正当化した。 |