Branching quantifiers in Trade Logic, part 1
Previously
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 axioms^{1} in Trade Logic formulas.
Branching quantifiers
The Internal Set Theory axioms require the predicate finite
. This
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 Q_{H}, then Q_{L} 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.
Q_{H}
The basic idea is that the "test" clause of if
is a conjunction of
the best
's of the two branches, while the formula dependent on all
the objects is the "then" clause. In Trade Logic, if
is always
singlebranched; it abbreviates (or (not A) B)
.
That almost works. The problem is that each branch actually nests two
applications of 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 as^{2}:
(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
variables, best_AE
.
(definepredicate (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 multibranched configuration, that subformula will only "see" the universal binding that dominates it, which is just what we need for branching quantifiers.
With best_AE
, we can define Q_H
. NB, the branches of the
conjunction output complementary arguments. First we'll define
best_H
:
(definepredicate (best_H Phi U +x_1 +x_2 +y_1 +y_2) (bindunordered (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))))
Sharpeyed readers will notice two things:
 Contradictory ordering requirements. We have to bind x_{1} before we can bind x_{2}, but also have to bind x_{2} before we can bind x_{1}.

New predicate
bindunordered
. 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.
Having defined best_H
, we can define Q_H
as simply:
(definepredicate
(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)))
Footnotes:
^{1} Why that? Just because I happen to like illimited numbers.
^{2} I've changed pred
to lambda
. It means the same. As I
wrote it more often, I realized that I preferred the familiar lambda
even if it does wrongly suggest a function.
No comments:
Post a Comment