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 x1 before we
can bind x2, but also have to bind x2 before we can bind x1.
-
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)))
