0

我想推理从有限集中选择一个元素的函数。

我试图定义一个谓词，告诉我某个给定函数是否是这样的“选择器”函数：

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
4

1 回答 1

2

我只是根据 Brian 的评论提供详细信息，即仅为非空集的集合定义选择函数。

来自关于 Choice_function 的 Wikipedia 条目：

选择函数 (selector, selection) 是一个数学函数 f，它定义在非空集合的某个集合 X 上，并将 S 的某个元素 f(S) 分配给该集合中的每个集合 S。

到目前为止，你可能已经从 Brian 的评论中得到了你需要的东西，但无论如何我都会这样做。的定义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

于 2013-09-14T23:33:13.290 回答