在命题作为类型中证明选择公理：ac函数定义的合理性验证

嘿，你的这个定义其实是完全正确的！不过我们可以拆解每一步的细节来确认，同时给出符合依赖类型论规范的严谨证明，让整个逻辑更清晰。

先快速回顾下命题作为类型的核心对应关系，这是理解整个证明的基础：

• 全称量词 ∀x:A. P x 对应依赖函数类型 Π_{x:A} P x
• 存在量词 ∃y:B. Q y 对应依赖和类型 Σ_{y:B} Q y
• 逻辑蕴涵 P → Q 对应函数类型 P → Q

所以选择公理的目标类型 (Π_{x:A} Σ_{y:B} R x y) → Σ_{f:A→B} Π_{x:A} R x (f x)，本质就是要构造一个函数：输入是「每个x都对应一个(y, p)（其中p是R x y的证明）」，输出是「一个函数f:A→B，加上一个证明：对所有x，R x (f x)」。

你的定义的正确性验证 #

你给出的 ac f := (fst ∘ f, snd ∘ f)，我们把它展开成类型论的λ表达式来核对每一部分的类型：

1. 第一个分量 fst ∘ f：其实就是 λx. fst (f x)。对于任意x:A，f x 是Σ类型的元素，fst (f x) 会提取出这个元素里的y分量（属于B），所以整个λ表达式的类型是 A → B，完全符合输出的第一个分量要求。
2. 第二个分量 snd ∘ f：也就是 λx. snd (f x)。对于任意x:A，f x 的类型是 Σ_{y:B} R x y，这意味着snd (f x) 的类型正好是 R x (fst (f x))——也就是 R x ((fst ∘ f) x)，所以这个λ表达式的类型就是 Π_{x:A} R x ((fst ∘ f) x)，完美匹配输出的第二个分量要求。

所以你的定义完全满足选择公理的类型约束，是正确的。

更严谨的形式化实现（以Agda/Coq为例） #

如果要写出完全符合依赖类型论工具规范的证明，比如在Agda或Coq中，我们可以这样展开：

Agda 写法 #

ac : {A B : Set} {R : A → B → Set} 
   → (∀ x → Σ B (λ y → R x y)) 
   → Σ (A → B) (λ f → ∀ x → R x (f x))
ac f = (λ x → fst (f x), λ x → snd (f x))

Coq 写法 #

Definition ac {A B : Type} {R : A -> B -> Prop}
  (f : forall x : A, exists y : B, R x y) :
  exists f' : A -> B, forall x : A, R x (f' x) :=
  exist (fun f' : A -> B => forall x : A, R x (f' x))
        (fun x => proj1_sig (f x))
        (fun x => proj2_sig (f x)).

这里的核心思路和你的定义完全一致：从输入的依赖函数中，分别提取每个x对应的y（作为目标函数f'）和对应的证明项（作为全称量化的证明），然后组合成Σ类型的结果。

最后要提一句：在构造主义类型论中，这个“选择公理”其实是可证明的定理，而不是像经典集合论那样的公理——因为我们是显式地从每个存在量词的证据中构造出了函数，不需要额外的假设。

内容的提问来源于stack exchange，提问作者Eben Kadile