Trade Logic: Branching quantifiers 2

Branching quantifiers in Trade Logic, part 2

Previously

Earlier I introduced Trade Logic. It's a form of logic that I designed to be suitable for connecting prediction markets. Last time, I built the branching quantifier Q_H in terms of Trade Logic, and now I'm going to build Q_L and Q_>=N

Q_L

Q_L (the Rescher quantifier) is a branching quantifier that basically means "less than or equal in number". That's one of the neat things that branching quantifiers can do that the classical quantifiers \(\forall\) and \(\exists\) can't.

As the description implies, we're going to need an equivalence predicate to build Q_L. Trade Logic deliberately doesn't provide a global equivalence predicate, so that will be a parameter.

For convenience, I'm also going to define iff (if and only if) as:

(or (and p q)(and (not p)(not q)))

It's not a predicate, because it takes formulas which are not an exposed type of object. With iff and Q_H, I can easily build Q_L. This is really just a transcription of the usual definition.

(define-predicate (Q_L 
                     U 
                     (the ,(pred thing thing) Equal) 
                     (the ,(pred thing) phi)
                     (the ,(pred thing) psi))
   (Q_H U
      (lambda (x_1 x_2 y_1 y_2)
         (and
            (iff (Equal x_1 x_2) (Equal y_1 y_2))
            (if (phi x_1) (psi y_1))))))

infinite aka Q_>=N

We can verbally define infinite sets as sets where no matter how many elements you enumerate, there is always another element. We'll treat that as an existential quantification outside a Q_L comparison. So I'll define infinite as:

(define-predicate (infinite U (the ,(pred thing thing) Equal) phi)
   (let
      ((p 
          (lambda (a)
             (Q_L U Equal phi
                (lambda (y) (and (not (Equal a y)) (phi y)))))))
      ;;"\exists a" around the entire Q_L part.
      (if (best p U +a) (and (phi a)(p a)))))

Side note: The LaTex formulas

I thought the LaTex formulas were formatting OK in Blogger because they looked OK in my previews. But apparently they're not. My mistake. I'll see if I can do something about them. But formatting math is not something I know a lot about.