Databases
StackOverflow2013
Postsdbo
POWhy is my definition of a function that chooses an element from a finite set inconsistent?
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POWhy is my definition of a function that chooses an element from a finite set inconsistent?
    primarykey
    data
    text
    <p>I would like to reason about functions that choose one element from a finite set.</p> <p>I tried to define a predicate that tells me whether some given function is such a “chooser” function:</p> <pre><code>definition chooser :: "('a set ⇒ 'a) ⇒ bool" where "chooser f ⟷ (∀ A . finite A ⟶ f A ∈ A)" </code></pre> <p>Actually those finite sets from which I'd like to choose elements are of a concrete type, but putting a concrete type in <code>'a</code>'s place causes the same trouble.</p> <p>I have also tried to omit <code>finite A</code>, but the sets I'm dealing with <em>are</em> finite, and I don't even want to think about the axiom of choice here.</p> <p>Now this definition seems to be inconsistent:</p> <pre><code>lemma assumes "chooser f" shows "False" using assms chooser_def by force </code></pre> <p>How can I define <code>chooser</code> in a reasonable way? I would like to use it as follows:</p> <pre><code>assume "finite A" moreover assume "chooser f" moreover assume "choice = f A" ultimately have "choice ∈ A" by ??? </code></pre> <p>Most of the time it merely matters <em>that</em> a member of the set is chosen, not <em>how</em> it is chosen.</p> <hr> <p>Background: I'd like to formalise tie-breakers in auctions (section 4 of <a href="http://arxiv.org/abs/1308.1779" rel="nofollow">this paper</a>). Suppose there are two highest bids for the item being auctioned, we need to arbitrarily choose the one bidder who should win the auction.</p> <hr> <p>Here is, BTW, a really minimal example (which is a bit harder to understand):</p> <pre><code>lemma "(∀ A . finite A ⟶ f A ∈ A) ⟹ False" by force </code></pre>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. USJonathan Leffler
    1. USChristoph Lange
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. COAssuming `chooser f`, doesn't that imply `f {} ∈ {}`?
      singulars
      1. POWhy is my definition of a function that chooses an element from a finite set inconsistent?
      1. USBrian Huffman
    2. COOops, indeed – thanks for spotting!
      singulars
      1. POWhy is my definition of a function that chooses an element from a finite set inconsistent?
      1. USChristoph Lange
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload