Branching quantifiers in Trade Logic, part 1
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.
As an experiment, I've been building towards writing the Internal Set Theory axioms1 in Trade Logic formulas.
The Internal Set Theory axioms require the predicate
can be built using branching quantifiers. If we had used the
"classical" quantifiers instead of
best, we'd need to add more
quantifiers now. Fortunately, branching quantifiers can be built with
best, unfortunately not in a straightforward way.
We're also going to have to extend the mode system. Earlier, I said
that the mode system required that there exist an ordering in which
all variables are bound before they are used. But branching
quantifiers bind variables simultaneously, in a sense. This sense is
more obvious when using
best, which requires applying the target
predicate, which means that each branch needs values that are bound in
the other branch.
We're going to start by building the simplest Henkin quantifier QH, then QL on top of that, then Q>=N which means infinite. All will be parameterized on U (a universal set). They latter two also parameterized on an identity predicate.
The basic idea is that the "test" clause of
if is a conjunction of
best's of the two branches, while the formula dependent on all
the objects is the "then" clause. In Trade Logic,
if is always
single-branched; it abbreviates
(or (not A) B).
That almost works. The problem is that each branch actually nests two
best. We could easily rearrange it to get the outer
variable, but we still need a way to retrieve the inner variable.
Each branch, if it were to exist in isolation, would be of the form $$ \forall x \exists y \phi(x,y) $$ which we write as2:
(let ;;Curried \exists y \phi(x,y) ((psi (lambda (X) (if (best (lambda (Y) (phi X Y)) U y_1) (Phi X y_1))))) ;;\forall x \psi (if (best (lambda (X) (not (psi X))) U x_1) (psi x_1)))
We'll define a slightly altered version of this that extract the
(define-predicate (best_AE phi U +x_out +y_out) (let ;;Curried \exists y \phi(x,y). Still consults \phi ((psi (lambda (X) (if (best (lambda (Y) (phi X Y)) U +y_out) (phi X y_out))))) ;;\forall x \psi. Doesn't consult \phi. (best (lambda (X) (not (psi X))) U +x_out)))
Note the resemblance between the formula for $$ \exists y \phi(x,y) $$ and a Skolemized variable. It takes a parameter, the same variable that $$ \forall x $$ binds. That means that when we incorporate this into a multi-branched configuration, that subformula will only "see" the universal binding that dominates it, which is just what we need for branching quantifiers.
best_AE, we can define
Q_H. NB, the branches of the
conjunction output complementary arguments. First we'll define
(define-predicate (best_H Phi U +x_1 +x_2 +y_1 +y_2) (bind-unordered (x_1 x_2 y_1 y_2) (and (best_AE (lambda (X Y) (Phi X x_2 Y y_2)) U +x_1 +y_1) (best_AE (lambda (X Y) (Phi x_1 X y_1 Y)) U +x_2 +y_2))))
Sharp-eyed readers will notice two things:
- Contradictory ordering requirements. We have to bind x1 before we can bind x2, but also have to bind x2 before we can bind x1.
bind-unordered. It works with the mode system and loosens the requirement that there exist an ordering in which all variables are bound before they are used. Within its scope, the ordering rules are suspended among the variables listed in the first argument. I'm not yet sure what the proper rules are for it. It's likely to block decomposition in most cases.
best_H, we can define
Q_H as simply:
(define-predicate (Q_H Phi U) (if (best_H Phi U +x_1 +x_2 +y_1 +y_2) (Phi x_1 x_2 y_1 y_2)))