Почему мое определение функции, которая выбирает элемент из конечного множества, несовместимо?

Question

Я хотел бы рассуждать о функциях, которые выбирают один элемент из конечного набора.

Я попытался определить предикат, который говорит мне, является ли какая-то данная функция такой функцией "выбора":

definition chooser :: "('a set ⇒ 'a) ⇒ bool"
where "chooser f ⟷ (∀ A . finite A ⟶ f A ∈ A)"

На самом деле те конечные множества, из которых я бы хотел выбрать элементы, относятся к конкретному типу, но помещают конкретный тип в 'a Это место вызывает те же проблемы.

Я также пытался опустить finite A, но сеты, с которыми я имею дело , конечны, и я даже не хочу думать об аксиоме выбора здесь.

Теперь это определение кажется противоречивым:

lemma assumes "chooser f" shows "False" using assms chooser_def by force

Как я могу определить chooser разумным образом? Я хотел бы использовать его следующим образом:

assume "finite A"
moreover assume "chooser f"
moreover assume "choice = f A"
ultimately have "choice ∈ A" by ???

Большую часть времени имеет значение только то, что выбран элемент набора, а не то, как он выбран.

---

Справочная информация: Я хотел бы официально оформить тай-брейки на аукционах (раздел 4 этой статьи). Предположим, есть две самые высокие ставки для предмета, выставляемого на аукцион, нам нужно произвольно выбрать одного участника, который должен выиграть аукцион.

---

Вот, кстати, действительно минимальный пример (который немного сложнее понять):

lemma "(∀ A . finite A ⟶ f A ∈ A) ⟹ False" by force

Answer 1

Я просто предоставляю подробности, основанные на комментарии Брайана о том, что функция выбора определяется только для набора непустых множеств.

Из записи в Википедии о Choice_function:

Функция выбора (селектор, выбор) - это математическая функция f, которая определена в некотором наборе X непустых множеств и присваивает каждому множеству S в этом наборе некоторый элемент f(S) из S.

К настоящему времени у вас, вероятно, уже есть то, что вам нужно от комментария Брайана, но я все равно делаю это. Определение chooser нужно только требование, чтобы набор не был пустым:

definition chooser :: "('a set => 'a) => bool" where 
  "chooser f <-> (!A. A ~= {} --> f A ∈ A)"

theorem "(finite A & A ~= {} & chooser f) ==> (f A ∈ A)"
by(metis chooser_def)

theorem "(A ~= {} & chooser f) ==> (f A ∈ A)"
by(metis chooser_def)

Вы сказали, что не хотите использовать Аксиому выбора, но стандартная функция выбора демонстрирует хороший шаблон для подражания, а не то, что он вам нужен.

definition choice :: "'a set => 'a" where
  "choice T = (SOME x. x ∈ T)"

theorem "T ~= {} ==> choice T ∈ T"
  by(unfold choice_def, metis ex_in_conv someI

--GC