自然数対象の射影性

定理（[Forssell–Lumsdaine–Swan 2026, 定理4.24]）: 自由トポス$\mathcal{F}$の自然数対象$N$は射影的である。

Nの射影性 とは、$N$上の全射$e:X\twoheadrightarrow N$が常に切断$s:N\to X$を持つこと。圏論的には「Nが射影的」$⟺$ $N$への任意の全射が分裂する。

系— 可算選択規則 (Rule of Countable Choice: ${\mathrm{RC}}_{\omega }$)

${\mathrm{IHOL}}_N$が"$\forall n:N\exists x:X\varphi (n,x)$" を証明するならば、ある${\mathrm{IHOL}}_N$で定義可能な関数$f:N\to X$が存在して"$\forall n:N\varphi (n,f(n))$" を証明する（[Forssell–Lumsdaine–Swan 2026, 系 4.25]）。

これは直観主義高階論理の規則（含意の形をしたメタ定理）であって公理ではないことに注意。

依存選択 (Dependent Choice: ${\mathrm{RC}}_{\mathrm{dep}}$)

同様に、依存選択規則も自由トポスで成立する（[Forssell–Lumsdaine–Swan 2026, 定理4.27] / [Forssell–Lumsdaine–Swan 2026, 系 4.28]）。

歴史

• Friedman–Scedrov (1983) が証明論的手法で解決
• Makkai (1980) が未発表ノートで圏論的（2-圏論的）証明を与えたが、長らく失われていた
• 2015年12月、Makkaiがストックホルムで原ノートを発掘
• Forssell–Lumsdaine–Swanによる再構成版が2026年に出版 (arXiv:2604.01139)

証明スケッチ

1. $\mathcal{F}$を階数$\infty$の自由トポス ${\mathcal{F}}_{\infty }$ に置き換える（[Forssell–Lumsdaine–Swan 2026, 命題 2.14]）
2. コンパクト性により、$N$上の任意の射は有限階数$r$の${\mathcal{F}}_r$に由来（[Forssell–Lumsdaine–Swan 2026, 命題2.6]）
3. 各$r$に対して、算術宇宙 (AU) が内部自由$r$-トポス${\mathbb{F}}_r$を持つ（[Forssell–Lumsdaine–Swan 2026, 定理3.23]）
4. 内部Freydグルーイングにより、${\mathbb{F}}_r$の終対象は射影的（[Forssell–Lumsdaine–Swan 2026, 定理4.21]）
5. ${\mathbb{F}}_r$の標準解釈$[[-]]$: ${\mathbb{F}}_r\to \mathcal{E}$ により外部化（[Forssell–Lumsdaine–Swan 2026, 命題4.18]）
6. Gödel番号付けにより各型が可算整列可能（[Forssell–Lumsdaine–Swan 2026, 系3.35]）→ 最小Gödel番号のwitnessを取る

Remark 4.19（[Forssell–Lumsdaine–Swan 2026, Remark 4.19]）: 完全な内部化はTarskiの定義不能性定理により不可能。有限階数の近似に制限することで回避。

不完全性定理との接続

Remark 4.19（[Forssell–Lumsdaine–Swan 2026, Remark 4.19]）の指摘: 不完全性は有限階数近似の極限として現れる。この構造は GL-provability-logic における証明可能性の階層と深く関連する可能性がある。

関連ページ

• free-topos
• ranked-topos
• freyd-gluing
• arithmetic-universe
• countable-choice-rule

出典

• 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