可算選択規則
RC_ω: IHOL_N が “∀n:N ∃x:X φ(n,x)” を証明するならば、ある IHOL_N で定義可能な関数 f: N→X が存在して “∀n:N φ(n,f(n))” を証明する。
これは**規則（rule）**であって公理ではない — φ に含まれる自由変数や他のパラメータがある場合でも成り立つメタレベルの性質。
自由トポスにおける RC_ω
N の射影性（定理 4.24）の直接の帰結として RC_ω が成立する（系 4.25）。さらに同様の手法で依存選択規則（RC_dep）も成立（定理 4.27/系 4.28）。