[CL] Correction and Question

[John F. Sowa]

Pat,

I realized that I need a universal quantifier over all
four arguments.

JS> But (IntegerDivide ?x1 ?x2 | ?x3 ?x4) becomes a CL
> relation with four arguments and with the following
> axiom to state the functional dependencies of x3 and x4
> on x1 and x2:
> 
>    (exists (f1 f2) (forall (x1 x2)
>        (IntegerDivide x1 x2 (f1 x1 x2) (f2 x1 x2))))

This doesn't rule out the possibility that x3 and x4
might have other values that aren't the results of
those functions.  Therefore,

    (exists (f1 f2) (forall (x1 x2 x3 x4)
       (iff (IntegerDivide x1 x2 x3 x4)
            (and (= x3 f1 x1 x2)) (= x4 (f2 x1 x2))))))

But it would also be possible to state that constraint
with the *exactly one* quantifier:

    (forall (x1 x2) (exists! (x3 x4)
       (IntegerDivide x1 x2 x3 x4)))

Without exists!, the formula becomes messier:

    (forall (x1 x2) (exists (x3 x4) (forall (x5 x6)
       (if (and (IntegerDivide x1 x2 x3 x4)
                (IntegerDivide x1 x2 x5 x6))
           (and (= x3 x5) (= x4 x6))))))

Is there a simple way of defining exists! and
other generalized quantifiers in CL?

John