2

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

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

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

只给定 α 非空的断言 h，选择 h 神奇地产生了 α 的一个元素。

现在，如果我阅读有关集合论和选择公理的文献（Jech）：

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

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

对我来说，这些东西似乎并不等同。有人可以详细说明一下吗？

4

1 回答 1

2

精益中的公理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)⟩

换句话说，这就是说：给定一系列非空类型（集合），选择函数的类型是非空的。如您所见，Lean's 的证明是直接的choice。

于 2019-03-29T15:54:53.223 回答