可算選択規則

${\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))$" を証明する。

これは規則 (rule) であって公理ではない— $\varphi$ に含まれる自由変数や他のパラメータがある場合でも成り立つメタレベルの性質。

自由トポスにおける${\mathrm{RC}}_{\omega }$

$N$の射影性（[Forssell–Lumsdaine–Swan 2026, 定理4.24]）の直接の帰結として${\mathrm{RC}}_{\omega }$ が成立する（[Forssell–Lumsdaine–Swan 2026, 系 4.25]）。さらに同様の手法で依存選択規則 (${\mathrm{RC}}_{\mathrm{dep}}$) も成立（[Forssell–Lumsdaine–Swan 2026, 定理4.27] / [Forssell–Lumsdaine–Swan 2026, 系4.28]）。

関連ページ

• projectivity-of-N
• free-topos
• freyd-gluing

出典

• 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