Trade Logic: Branching quantifiers 1

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¹ 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 single-branched; 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²:

(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.

(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.

With best_AE, we can define Q_H. NB, the branches of the conjunction output complementary arguments. First we'll define best_H:

(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 x₁ before we can bind x₂, but also have to bind x₂ before we can bind x₁.
• New predicate 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.

Having defined 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)))

Footnotes:

¹ Why that? Just because I happen to like illimited numbers.

² 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.