Re: cheating about reification

Pat Hayes wrote:
> ...
> Right, but one would not use IEXT for reification. I introduced a
> REIF mapping from the syntax into IR, but one could do it more simply
> just by requiring IR to contain a suitable set of expressions, by
> semantic fiat, so that REIF is defined to be the identity.
> 
> >
> >What about the following addition to the MT. Let a ternary relationship
> >Reif be defined as:
> >
> >1) IR x IR x (IR union LV) <= Reif
> >2) If (x,y,z) in (IR union Reif) x IR x (IR union LV union Reif),
> >    then (x,y,z) in Reif
> >3) Reif is the smallest set with (1), (2)
> >
> >In other words, Reif contains all reified statements that can possibly
> >be constructed under a given interpretation I.
> 
> Right, that is almost the version I had at the F2F. (I used a mapping
> from the syntax into the domain, you use a three-place predicate
> defined recursively on the domain.) However, it was resoundingly
> criticized as not what reification actually means, in practice. (Dan
> C. told me that this was what reification *ought* to have been, but
> in fact it wasn't that.) I am still waiting to discover what
> reification actually is, in practice (as opposed to what the M&S says
> it is.)

Maybe the confusion arose because in your original version reification
mapped directly from the syntax. I must confess that I thought (and
possibly other F2Fers did) that your definition treated reification as
some kind of special syntactic mapping that needs to be established in
addition to I. Of course, from the logical perspective both approaches
may well be equivalent. However, reification as defined above is easier
to capture by people with limited background in logics like me. The
above definition suggests that all reified statements always exist in
each interpretation of a given set of statements. It's just that there
is no a priori relationship between those reified thingies and the other
resources in the domain of discourse. Then, special-purpose vocabularies
like rdf:subject, rdf:object etc. could be introduced to define such
relationship. I guess all this is obvious for you...

> >Now we have some
> >"thingies" to reason about. By the way, it can be shown that the set
> >Reif indeed exists, but the proof is non-trivial.
> 
> Its just a variation on Herbrand's theorem. If you want to get very
> strict, you need the second recursion theorem, I guess, but I'm
> willing to just accept that the syntax BNF has a minimal fixedpoint,
> and take that as read; after all, without that assumption, there
> isn't a language there to give a semantics to in the first place.

Excellent! That makes life even easier. In fact, the proof that you
suggest hints that reification is more like a mapping from some kind of
syntax, supporting your point. Still, I think it has certain didactical
benefits to settle reification directly within DD.

Do you think it's worth a try to revamp reification in a manner similar
to the above and sell it again to the WG? I'd support you, I promise ;)

Sergey

Received on Thursday, 25 October 2001 11:54:30 UTC