Определение выбора в Lean
В Lean "выбор" реализуется в соответствии с:
Наша аксиома выбора теперь выражается просто следующим образом:
axiom choice {α : Sort u} : nonempty α → α
Учитывая только утверждение h о том, что α непусто, выбор h магически порождает элемент α.
Теперь, если я читаю литературу (Jech) по теории множеств и аксиоме выбора:
Аксиома выбора (AC). Каждое семейство непустых множеств имеет функцию выбора.
Если S - семейство множеств и ∅ не в S, то функция выбора для S - это функция f на S, такая что f(X) ∈ X для любого X ∈ S.
Мне эти вещи не кажутся эквивалентными. Может кто-нибудь уточнить это?
0 ответов
Аксиома choice в Lean действительно не совпадает с axiom of choice в теории множеств. Аксиома choice в Lean на самом деле нет соответствующего утверждения в теории множеств. Что говорит то, что есть функция, которая берет доказательство того, что какой-то тип α непуста и производит жителя α, В теории множеств мы не можем определить функции, которые принимают доказательства в качестве аргументов, поскольку доказательства не являются объектами в теории множеств, они находятся в слое логики поверх этого.
Тем не менее, две аксиомы выбора не полностью не связаны. Из Аксиомы Leans 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,