10 August 2011

Trade Logic: Branching quantifiers 2

Branching quantifiers in Trade Logic, part 2


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 (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 
                     (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)
            (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)
          (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