All objects are sampleable
I mentioned earlier in passing that in trade logic, all things are
sampleable. As I put it, "all variables are ultimately
Things can be finite sets of objects with some probability distribution over them. They can be trivially sampleable, such as single objects, where sampling them always gives the same object. It's even possible that they may measureable collections that have no distinct individuals, from which one selects measured extents.
And the time has come to nail down how Trade Logic is to do sampling (selection).
For a population to be sampled, we need some sort of random input, and
it can't be vague where to get the random or how to use it. The
pick01 is to provide the random parameters that sampling
(pick01 +A) binds A to a real number between 0 and 1,
lower-inclusive. Theoretically, A has infinite precision. In
practice, precision should be provided lazily. There may need to be
some provision against allowing requests for precision to tie up the
I'll call a bet whose formula uses
pick01 (explicitly or implicitly)
population bet. Population bets are useful for propositions that
can easily be resolved for individuals but less easily for
Population bets that are trying to be resolved1 can pick particular individuals to resolve. Then they can settle probabilistically on the basis of that. It's basically using statistics.
The procedure for selecting an individual is to:
independently choose a value for each
pick01directly or indirectly included in the proposition.
- Using those values, assess the issue's truth or falsity. (The Bettable selectors logic below should ensure that this step works)
- Repeat as wanted. We sample with replacement; for simplicity and generality, there is no provision for not looking at the same individual again.
- Using statistical logic (outside the scope here), settle the bet (maybe sometimes just partly settle it)
Of course randoms on the unit interval are not the only kind of random selection one might want. We have to build all sorts of selectors from them. At the same time, we want selection to be uniquely resolved. It won't do for a given selector to select more than one individual for the same randoms, or to select no individual at all.
So I introduce a different sort of bet:
selector bets. They are
bets that a given selector "works OK".
Any predicate that has only outputs can be the basis of a selector bet. In my current thinking, for each such bet, every output of the predicate would be associated with an equivalence predicate. That's needed so we have a principled way to distinguish individuals.
Unlike issues, the bet is asymmetric and its interpretation is
adversarial: One side (challengers) tries to pick values for
that they think give no result or too many results. The other side is
betting that no such problems arise. I haven't fleshed out the exact
rules for this.
It seems that I didn't adapt
epsilon enough when I borrowed it as
best. It doesn't make a sampleable output. Rather, its output is
the set of all the most suitable objects in the universe. That's not
neccessarily finite, much less measureable. So there's no good
general distribution over that. It would be paradoxical if there
best needs another parameter: a sampleable collection of objects.
That can be any object in Trade Logic. This parameter will generally
be quite boring; often it's simply the whole universe of discourse.
Nevertheless, it's needed.
So =(best Pred From To)=2 is now true just if:
Predis a unary predicate
Tois the part of
Predas well as anything else in From does
NB, I have not called
To a "member" of
From, as if
From were a
set. In general,
From is a collection.
To should be collection
in general too. And we don't want to need an identity predicate as
another parameter. And finally, we don't try to resolve "sub-part
boundaries" here; those are addressed via structurally similar bets
that replace calls of
best with suitable particularizations.
Nevertheless, I am not 100% sure I have supported collections
adequately in this mechanism.