[SCL] [CL] Quantifying over propositions

[Sandro Hawke]

> > Oh!  In other words, Pat was using brackets
> > as a method of quoting:
> > 
> >  > (forall (p) (implies (believes john p) (= p [round earth])))
> 
> I'm not sure that's what he was doing; I was a bit confused by that
> notation, and need to go back and read the relevant message more
> carefully to see what Pat was up to.
>  
> > Then we're in agreement.  I always insisted that we need
> > at least a quote and preferably a backquote, as in KIF.
> 
> Those will be needed for CL-meta -- for talking about languages.  The
> square brackets are term forming operators for talking about
> propositions.  Those are quite different (as you know).

Perhaps you can enlighten the rest of us?   :-)  

The KIF dpans includes the example:

    (believes john '(material moon stilton))
    (=> (believes john ?p) (believes mary ?p))

which looks very similar to me.

Also, I'm curious why square brackets?  Personally, I'd like curly
brackets, which seem to be used to enclose (if not exactly quote) bits
of the top-level language in many languages, such as C, Java, and
Perl.  I also love having square brackets for lists in Prolog and
prolog-like FOL syntaxes like Otter.  [I don't mean to provoke a
syntax war of course!  Just kind of wondering how you approach this
stuff.]

(I've been lurking on this list for a while.  For those who don't know
me, I'm the lead on the W3C rule language work [1], and I'm very
interested in this stuff, but I'm not a logician.  Sorry if I'm using
the list incorrectly.)

       -- sandro

[1] http://www.w3.org/2004/12/rules-ws/report/