0

有限集合から 1 つの要素を選択する関数について推論したいと思います。

特定の関数がそのような「選択」関数であるかどうかを示す述語を定義しようとしました。

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 )。オークションにかけられているアイテムに 2 つの最高入札額があると仮定すると、オークションに勝つべき 1 人の入札者を任意に選択する必要があります。

これは、ところで、本当に最小限の例です（これは少し理解しにくいです）：

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

1 に答える 1

2

選択関数は空でないセットのコレクションに対してのみ定義されるというブライアンのコメントに基づいて、詳細を提供するだけです。

Choice_function に関するウィキペディアのエントリから:

選択関数 (セレクター、選択) は、空でないセットのコレクション X で定義され、そのコレクション内の各セット S に S の要素 f(S) を割り当てる数学関数 f です。

ここまでで、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 に答える