## 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.

## No comments:

## Post a Comment