- From: pat hayes <phayes@ai.uwf.edu>
- Date: Mon, 10 Sep 2001 20:19:21 -0500
- 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 UTC