Pseudo-quantification in Trade Logic via
Earlier I introduced Trade Logic. It's a form of logic that I designed to be suitable for connecting prediction markets. It is logic that "lives" within the system, not in individual traders' analyses.
Trade Logic doesn't use quantification as such. Quantification would
complicate the mode system, which is already adequate to distinguish
free and bound variables. I also have theoretical concerns about
vacuous quantification: If there were no objects that the system could
refer to, the relative valuation of
(forall x (p x)) and
(some x (p x)) would be reversed.
Instead of directly using quantification, Trade Logic uses the
best, which is adapted from Hilbert's
best(A,B) is true just if:
- B is a unary predicate
- A satisfies B as well as anything else does
I'll expand a little on that last point. That's not the same as
best can be true if no value could satisfy B. In
best can also be true in fuzzy ways:
If B can only be satisfied to a certain degree, and A satisfies B
to that degree, then
best(A,B)is true (crisply, 100%)
if A satisfies B to a certain degree, but a lesser degree than some
other value would, then
best(A,B)is fuzzily true
Quantifiers can be expressed in terms of
best, as they could with
epsilon. In standard notation, we would write:
In Trade Logic, the respective formulas are:
(if (best +x (lambda (Y) (not (-p Y)))) (-p -x))
(if (best +x -p) (-p -x))
Note the addition of modes, and note that "p" is always an in mode. It must be bound outside this (sub)formula.
The behavior of
yes of any issue of the form
(best +A -B) can be converted to a
(& (-X +A) (-B -A)) for any predicate X. Similarly, a
(& (-X +A) (-B -A)) can be converted to a
(best +A -B).
X may select
A in an arbitrary way, but it will never be better at
(best +A -B) is.
This works because no trader would make this conversion unless he got
a better price after the conversion. This ensures that the price of
best issues is always in fact the highest price. Effectively,
existentially quantified issues are always as high or higher in price
than each of their particular instances, and universally quantified
issues as low or lower than their particular instances.
It is a function
- Usually it comes with an axiom of extensionality, ie that the function's result is unique.
- It takes one argument, a predicate (as a formula)
- If that predicate can be satisfied, it returns an object that satisfies the predicate
- If that predicate can't be satisfied, it returns any object at all.
- With it, one can build statements equivalent to other statements that contain universal and existential quantifiers.
somecan be expressed using it.
1 When I first saw Epsilon, I got the impression that it wasn't suitable for this reason. But I was wrong, it just needed to be adapted.