W3C home > Mailing lists > Public > w3c-rdfcore-wg@w3.org > September 2001

Re: namedNode? in predicate position?

From: pat hayes <phayes@ai.uwf.edu>
Date: Mon, 10 Sep 2001 20:19:21 -0500
Message-Id: <v04210113b7c3161ef4a8@[205.160.76.173]>
To: jos.deroo.jd@belgium.agfa.com
Cc: w3c-rdfcore-wg@w3.org
>[...]
> >> I have also found that to describe RDF-schema-based inferences, I
> >> have wanted to construct expressions in which the RDF property is a
> >> "variable".  I think the required effect could be achieved by means
> >> other than "princeNode" arcs, but maybe less intuitive for a
> >> developer.
> >
> > Yes, others have noted this also. OK,  this also can be allowed in
> > the syntax without changing the MT; but I think that if we do allow
> > this then I ought to rewrite the model theory slightly, because as it
> > stands right now its not  quite clear what this would mean. The MT
> > uses a standard logical device to describe existentials, basically
> > saying that the existential is true
>
>I would think *the assertion containing* the existential has a
>truth value, not the existential itself

Right. Sorry, I was being sloppy: people talk of 'existential 
quantifer' and 'existential statement' and I tend to use the one that 
is handiest.

>
> > if there is some interpretation
> > of what it denotes that makes the assertion true. The trouble with
> > this trick for relations (properties) is, that the simple denotation
> > of a property isn't really all that important: what makes assertions
> > involving it true or false are the *extensions* of those denotations.
> > So a lot turns on whether those extensions are allowed to change when
> > the denotation of the anonymous node is allowed to change.
>
>I would think so, yes

Oh, I hope not. If so, then the quantifier over properties isn't over 
the properties themsleves (which is still first-order) but over their 
possible extensions (which is higher-order and not semidecideable). 
That would mean that the proof process would have to be able to 
handle unification of expressions with embedded lambda-expressions, 
for example. Best to not go there, believe me.

>
> > The only
> > way to interpret this that would produce a reasonable proof theory
> > would be to take the extension mappings as fixed and let just the
> > denotations vary; which is what the MT says right now, in fact, but
> > it ought to say it much more clearly and explicitly, since a lot
> > hangs on that point if we are going to allow princeProperties.
>
>that's nice
>and again, thanks for the thing/extension distinction!

Thanks due to Chris Menzel for that one.

Pat

---------------------------------------------------------------------
(650)859 6569 w
(650)494 3973 h (until September)
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes
Received on Monday, 10 September 2001 21:17:59 EDT

This archive was generated by hypermail pre-2.1.9 : Wednesday, 3 September 2003 09:39:41 EDT