## 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 QH in terms of Trade Logic, and now I'm going to build QL and Q>=N

### QL

QL (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 QL. 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 QH, I can easily build QL. 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 QL 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.