精益选择的定义

Question

在精益中，“选择”是根据以下原则实施的：

我们的选择公理现在简单地表述如下：

axiom choice {α : Sort u} : nonempty α → α

只有断言h是非空的，选择h才能神奇地产生一个α元素。

现在，如果我阅读关于集合论和选择公理的文献(Jech)：

选择公理(AC)每个非空集族都有一个选择函数。

如果S是一个集合族，且S不是S中的∅，则S的选择函数是S上的函数f，使得f(X)∈X对每个X∈S。

在我看来，这些东西似乎是不一样的。有人能详细说明一下吗？

Answer 1

精益中的公理choice确实不同于集合论中的axiom of choice。精益中的公理choice在集合论中实际上没有相应的表述。也就是说，有一个函数可以证明某种类型的α是非空的，并生成α的居民。在集合论中，我们不能定义以证明为论据的函数，因为证明不是集合论中的对象，而是在逻辑层之上。

也就是说，这两个选择公理并不是完全无关的。通过倾斜公理choice，您可以从集合论中证明比较熟悉的选择公理，这是一个可以找到这里的版本。

theorem axiom_of_choice {α : Sort u} {β : α → Sort v} {r : Π x, β x → Prop} (h : ∀ x, ∃ y, r x y) :
  ∃ (f : Π x, β x), ∀ x, r x (f x)

在库的其他部分中，证明了与选择公理相同的其他语句，如每个满射函数都有一个右逆。。

也许最接近您所引用的选择公理版本的语句如下：

theorem axiom_of_choice' {α : Sort u} {β : α → Sort v} (h : ∀ x, nonempty (β x)) : 
  nonempty (Π x, β x) :=
⟨λ x, classical.choice (h x)⟩

换句话说，这说明:给定一个非空类型(集合)，选择函数的类型是非空的。正如你所看到的，这个证据是从精益的choice中直接得到的。