N の射影性
定理（4.24）: 自由トポス ℱ の自然数対象 N は射影的である。
N の射影性とは、N 上の全射 e: X ↠ N が常に切断 s: N → X を持つこと。圏論的には「N が射影的」⇔ N への任意の全射が分裂する。
系 — 可算選択規則 (Rule of Countable Choice: RC_ω)
IHOL_N が “∀n:N ∃x:X φ(n,x)” を証明するならば、ある IHOL_N で定義可能な関数 f: N→X が存在して “∀n:N φ(n,f(n))” を証明する（系 4.25）。
これは直観主義高階論理の規則（含意の形をしたメタ定理）であって公理ではないことに注意。
依存選択 (Dependent Choice: RC_dep)
同様に、依存選択規則も自由トポスで成立する（定理 4.27 / 系 4.28）。
歴史
- Friedman–Scedrov (1983) が証明論的手法で解決
- Makkai (1980) が未発表ノートで圏論的（2-圏論的）証明を与えたが、長らく失われていた
- 2015年12月、Makkai がストックホルムで原ノートを発掘
- Forssell–Lumsdaine–Swan による再構成版が 2026年に出版 (arXiv:2604.01139)
証明スケッチ
- ℱ を階数 ∞ の自由トポス ℱ_∞ に置き換える（命題 2.14）
- コンパクト性により、N 上の任意の射は有限階数 r の ℱ_r に由来（命題 2.6）
- 各 r に対して、算術宇宙（AU）が内部自由 r-トポス 𝔽_r を持つ（定理 3.23）
- 内部 Freyd グルーイングにより、𝔽_r の終対象は射影的（定理 4.21）
- 𝔽_r の標準解釈 ⟦−⟧: 𝔽_r → ℰ により外部化（命題 4.18）
- Gödel 番号付けにより各型が可算整列可能（系 3.35）→ 最小 Gödel 番号の witness を取る
Remark 4.19: 完全な内部化は Tarski の定義不能性定理により不可能。有限階数の近似に制限することで回避。
不完全性定理との接続
Remark 4.19 の指摘: 不完全性は有限階数近似の極限として現れる。この構造は GL-provability-logic における証明可能性の階層と深く関連する可能性がある。