Branching quantifiers in Trade Logic, part 2
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
(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.