算術宇宙

定義（[Forssell–Lumsdaine–Swan 2026, 定義3.21]）: 算術宇宙 (AU) とは、リスト付き余完備前トポス (list-arithmetic pretopos)— すなわち、余完備性（有限余極限）とパラメータ化リスト対象を持つ局所有限余完備圏 (locos) であって、さらにexactなもの。

トポスより弱い構造で、冪対象 (power-object) を仮定しない。その代わりにリスト対象（自然数や帰納的データ型に対応）を持つ。

重要性

• 算術宇宙上の内部トポス: 任意の算術宇宙$\mathcal{E}$は、内部言語で記述された初期内部strict $r$-トポス${\mathbb{F}}_r$を持つ（[Forssell–Lumsdaine–Swan 2026, 定理3.23]）
• AU-論理関手はこの内部トポスを保存する
• Gödel番号付け（[Forssell–Lumsdaine–Swan 2026, 系3.35]）: 各内部$r$-トポスの各型はAU内で可算 (enumerable)

これにより、圏論的内部化 (cirernalization) が可能になり、有限階数の近似をトポス内部で扱えるようになる。

関連ページ

• free-topos
• ranked-topos
• projectivity-of-N

出典

• Forssell, H., Lumsdaine, P. L., & Swan, A. W. (2026). Makkai’s Lost Proof of Projectivity of N in the Free Topos. arXiv:2604.01139v2 [math.LO]. https://arxiv.org/abs/2604.01139