Аксиома выбора это теорема

В теории типов, конечно. Сегодня в нашем тавтологическом кружке для самых маленьких азы зависимых типов мимоходом. Аксиома выбора может быть сформулирована по-разному, например так: для любого семейства непустых множеств A существует функция выбора f, определённая на A. Берем мы кучу непустых множеств, вводим индексацию, т.е. каждое множество из этой кучи соотносим с элементом из некоторого множества А, например, числом; получили семейство множеств. Для конечного набора множеств используем конечное множество индексов А, для счетного множества множеств - счетное множество индексов, например A=Nat, можем даже взять континуум разных множеств и адресовать их вещественными числами, так у нас в семействе даже будет множество с индексом Пи. Сами множества в семействе могут быть очень разной природы. Перейдя от множеств к типам, мы получаем семейство типов, индексированное типом А, т.е. для каждого х из А у нас будет тип B_x, для разных х тип может быть разным, и собрание всех этих B_x будет нашим семейством типов, зависимым типом. Исходное семейство множеств мы можем представить бинарным отношением R(x,y), где x из А, а y из B_x. Факт того, что это семейтсво непустых множеств, можно выразить требованием для R быть left-total: для каждого х из А обязан существовать хотя бы один y из B_x, для которых выполнено отношение R(x,y). Тогда из наличия такого вот отношения R следует существование функции f из А в B_x, которая для каждого х из А выбирает некоторый элемент y из множества B_x, для которого выполнено R(x,y). Это и есть аксиома выбора, и сейчас мы ее докажем конструктивно как теорему. Математически утверждение выглядит так:

(∀x:A . ∃y:B_x . R(x,y)) => (∃f : A -> B_x . ∀x:A . R(x, f x))

Запишем это утверждение и его доказательство на ЯП с зависимыми типами Idris. ( Read more... )