[SCL] [CL] Quantifying over propositions

[Chris Menzel]

On Fri, Aug 12, 2005 at 04:21:21PM -0400, Sandro Hawke wrote:
> > > 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.

Yes, Sandro, they are similar!  But there are three threads to pull
apart here:

(1) Quotation
(2) Back quotation (a.k.a. corner/quasi-/Quine quotation)
(3) Propositional reification

KIF has (1) and (2).  The example above is an instance of (1), plain
quotation.  Quotation takes an expression and forms a name for that
expression.  Such quotation is "opaque" -- spaces nothwithstanding,  the
resulting term is a closed syntactic block and doesn't allow quantifiers
to bind variables within the quoted expression; you might as well try to
bind the "x" in "Alexander".  Thus, in

(4)  (exists (?x) (believes john '(material ?x stilton)))

the quantifier is as vacuous as in

(5)  (exists (?x) (believes john '(material moon stilton)))

To allow for quantifying in, KIF uses backquotes, which work
semantically similar to backquotes in LISP; a backquoted expression
containing a quantified variable X, for a given value E of that
variable, refers to the expression resulting from substituting E for X.
This is very convenient for doing metatheory, when one wants to quantify
over large classes of expressions.  Thus, for example, the existential
clause in a definition of truth for a given language L relative to a
give model M with domain D could be stated as follows:

(forall (?var ?formula)
        (and (Variable ?var)
             (Formula ?formula)
        (iff (True M `(exists (?var) ?formula))
             (exists (?obj)
                     (and (member ?obj D)
                          (True (Variant M ?var ?obj) ?formula))))))

where (Variant M ?var ?obj) is the model just like M except that ?obj is
assigned to the value of the variable assigned to ?var.  Note the
backquote here allows us to assign appropriate values to "?var" and
"?formula", viz., a variable and a formula of L.

But note that using backquote in an intensional context like John's
belief above really screws things up.  For if we replace the quote in
(5) with a backquote:

(6)  (exists (?x) (believes john `(material ?x stilton)))

the truth conditions are intuitively wrong.  For intuitively, (6)
expresses the proposition that there is something -- namely, let's
suppose, the moon -- that John believes to be made of stilton.  But on
the semantics of backquote, the moon cannot be the value for the
variable "?x" that makes (6) true, as the moon is not a linguistic
object!  It makes no sense to "substitute" the moon for the variable
"?x" in "(material ?x stilton)))".  Thus, to capture John's belief
correctly, we have to assume that the value of "?x" that makes the
sentence in question true is the NAME "moon".  

Now maybe some folks are willing to live with those truth conditions,
but note that it still leaves a problem, in that it requires anything
about which one might have a "de re" belief like (6) that involves
quantifying in to the belief context to be named in our language, aa
very strong and unparsimonious assumption.

But, really, it's not even a tenable option.  For not only do we get odd
truth conditions using backquoted expressions in belief contexts, we get
the wrong truth *values* in some cases.  For if John believes the moon
is made of stilton, he believes a heavenly body is made of stilton:

(7)  (exists (?x) (and (HeavenlyBody ?x)
                       (believes john `(material ?x stilton))))

But now we need the moon to be the value of the first bound occurrence
of "?x" and the name "moon" to be the value of the second occurrence;
i.e., there is no way to make (7) true on the quasi-quotation semantics.

For cases like the above, reified propositions work better.  Like
backquoted terms, proposition-denoting terms allow quantifying in, but
they seem to give us intuitively correct truth conditions.  In
particular, using square brackets to form proposition-denoting terms,
"[material moon stilton]" refers to the *reified proposition* that the
moon is made of stilton, not to a linguistic expression.  Consequently, 

(8)  (exists (?x) (and (HeavenlyBody ?x)
                       (believes john [material ?x stilton])))

is true just in case there is a heavenly body -- namely, the moon, in
this case -- that John believes to be made of stilton.  Intuitively, in
addition to getting the true value right, this approach captures the
"aboutness" of John's belief correctly; the thing that makes it the case
that John believes something is made of stilton is the *moon*, not the
name "moon".

Furthermore, there is no need to assume that everything is named.  (8)
would be true even if John's belef pertained to some heretofore
un-named heavenly body in the night sky.

> Also, I'm curious why square brackets?

No particular reason beyond the fact that they are commonly used to
form terms for reified propositions in a lot of the literature in
philosophical logic.  But bear in mind we are talking about CL here, so
the surface syntax is irrelevant; CL would only require that one have
term-forming operators that do the job; one can then let one's
individual preferences rule!

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

No, glad to have you!  You raise a very important question.  I hope the
above is useful and at least partly true. 8-)

-chris