large OWL structures (was: Re: new version of semantic layering document)

>[...]
>
>>  >>  >- There are many restrictions in Large OWL that may be 
>>problematic because
>>  >>  >   their presence may affect their extension.  For example, what is the
>>  >>  >   class extension of
>>  >>  >       _:x owl:onProperty rdfs:subClassOf .
>>  >>  >       _:x owl:maxCardinality 57 .
>>  >>
>  > >>  Its the class of all RDFS classes which have no more than 57
>  > >>  subclasses, right? That might be empty, for all I know. (Oh no, wait,
>  > >>  all the empty classes are in it.) But Im sure it *exists*. In fact,
>>  >>  you could toss in things like transfinite cardinalities (as long as
>>  >>  they are describable) and I would still be sure the restriction
>>  >>  classes would exist.
>>  >
>>  >>  >   Can it be shown that there are *no* problems in 
>>determining the class
>>  >>  >   extensions of all the restrictions that mention the RDF and RDFS
>>  >>  >   structural properties and that thus may interfere with 
>>their own class
>>  >>  >   extension?
>>  >>
>>  >>  Im not sure what you mean by 'interfere with'. One can certainly
>>  >>  create inconsistencies by asserting that, say, rdfs:subClassOf is the
>>  >  > same as some odd restriction. But just defining new restriction
>>  >  > classes in terms of the RDFS/OWL vocabulary doesn't in itself
>>  >  > interfere with that vocabulary in any sense I can think of.
>>  >
>>  >In Large OWL the class of all classes with no more than n subclasses
>>  >exists in all interpretations, for n any non-negative integer.
>  >
>>  Right. Some of them might be empty, of course. And one needs to be
>>  careful about 'all classes'; the universe is required to be closed
>>  under formation of restrictions, but it might not contain all the
>>  sets that a set-theorist might want to believe in.
>>
>>  >Some of
>>  >these classes may be subclasses of some other of them.  Can you show that
>>  >there is not some interaction between all these classes, and other such
>>  >Large OWL restrictions, that makes it impossible to have a consistent view
>>  >of all such OWL classes?
>>
>>  Im not sure what you mean by interaction. Of course there is no
>>  guarantee that any particular large-OWL graph will be consistent. But
>>  some of them will be, for sure. For example,
>>
>>  _:x owl:onProperty _:x .
>>  _:x owl:allValuesFrom _:x .
>>  _:x rdf:type owl:transitiveProperty .
>>  _:x owl:disjointWith owl:Nothing .
>>
>>  is large-OWL consistent: it can be satisfied by an interpretation
>>  whose 'core' (ie apart from all the RDFS machinery) is this:
>>
>>  IR= IC= {a,b}+IOR, IOR = {<a,{a}>,<a,{ }>}, IRP(x) = a
>>  IP={a}
>>  ICEXT(a)={a}, ICEXT(b)={ } (just to provide an empty class) and
>>  ICEXT(<x,y>)=y in IOR
>>  IEXT(a)={<a, a>}
>>  IEXT(I(owl:allValuesFrom))={<a, a>, <b, b>}
>>  and similarly for the others, and
>>  IEXT(I(owl:minCardinality)) = {<0, a>, <1, b>, <2, b>,....}
>>  and also similarly for the others, and the obvious extensions for the
>>  unions and intersections and so on. The universe needs to be
>>  populated by a lot more entities for the OWL and RDFS vocabulary to
>>  denote, but they don't need to be in any of the class or property
>>  extensions so they won't affect the closure conditions. For example,
>>  I(rdf:subClassOf) has got to be something, but all that really
>>  matters about it is that IEXT(I(rdfs:subClassOf)) = {<a, a>, <b, a>}.
>
>You have not nearly shown that this can be completed to a Large OWL
>interpretation.

You are a very hard man to please, Peter.

>What is the class extension of the required domain element
>that consists of precisely those domain elements that have at most 57
>superclasses, for example?

I think it is {a}, but I confess to not being entirely certain until 
I have checked the details

>
>>  I tell you what, If I define a complete satisfying interpretation for
>>  this plus the entire RDFS/OWL vocabulary, in full detail, will that
>>  satisfy you? It will take me a day or so.
>
>That would be a start.  However, you need an interpretation for *all* the
>OWL restrictions that are in every Large OWL interpretation.

Right, I realize that. That is why it will take me a day or so. I 
need to consider things like

_:x owl:onProperty owl:onProperty .

for example.

>This would
>mean that Large OWL would not be trivial.

I never said it was trivial.  RDFS isn't trivial. What I am certain 
of, and what seems kind of obvious to me, is that these structures 
always exist. Look, how could they possibly not? Almost every 
mathematical structure ever thought of can be constructed, perhaps in 
simulacrum, in ZF-AC. The only significant exceptions are Topos 
constructs, and those only because they make exorbitant claims to 
being both extraordinarily infinite and completely self-describing. 
There is nothing in OWL remotely like this; and even the Topos can be 
fitted into ZF+AC if one is willing to admit that certain large 
categories can be thought of as sets. The entire OWL/RDFS universe 
fits inside the iterated power set of IR, for goodness sake. None of 
this is very hard mathematics, just tedious.

>
>However, even that would not be enough.  For example, suppose that I say
>
>	ex:Person owl:subClassOf _:x .
>	_:x owl:onProperty ex:parent .
>	_:x owl:allValuesFrom ex:Person .
>
>which would be a natural thing to say about people.  Is this a
>contradiction in Large OWL?

No. I will sketch you a satisfying interpretation after dinner. In 
fact there is one in an earlier message, where the set/property a is 
equinumerous with its own class of subclasses.

>  If it is, then Large OWL is not very useful,
>though it might be non-trivial.  You would have to show that such natural
>OWL graphs are not contradictions.
>
>>  >The kind of problem that you could get into is if there was some break
>>  >point where ``less than n subclasses'' was empty but ``less than n+1
>>  >subclasses'' was not, except that the existence of  ``less than n
>>  >subclasses'' messed up this reasoning.
>>
>>  The basic point is that all these constructions fit within standard
>>  ZF+AC set theory, so as long as the basic domains are all sets -
>>  which they are by decree - then certainly the required semantic
>>  *structures* exist which satisfy all the closure rules, given all the
>>  basic interpretation machinery  (the IEXT, IRP, ICEXT mappings and so
>>  on).
>
>I don't buy this.

Well, tell me what you think is wrong with it. It seems obvious 
enough to me. We start with some sets, and some mappings over them. 
We then need to be certain the the closure of those sets under those 
mappings exists. How could it not? When I asked you a few weeks ago 
why these issues didnt crop up in your MT for abstract OWL, you said 
they just didnt arise, which is in a sense true, but in that very 
same sense they do not arise here either. They don't arise because we 
no longer feel the need to constantly prove that sets exist. We know 
that it makes sense to talk about the sets defined in terms of other 
sets in 'reasonable' ways. We know that ZF+AC can establish the 
existence of almost any set that anyone will ever want. It can 
certainly handle restrictions defined over the positive integers and 
functions on subsets of a fixed set, which is all that OWL needs.

>
>>  Whether or not that basic machinery can be so arranged as to
>>  satisfy all the triples of a particular graph is of course a
>>  different question.
>
>Agreed, but that is not what I am trying to get at.
>
>>  It might be worth rewriting the MT so as to make this
>>  structure/interpretation distinction more clear. That is the standard
>>  way to do it, as you know, but I thought it was too formal for the
>>  RDF MT. Now we have gotten this complicated, maybe that needs to be
>>  re-thought. The idea would be to have semantic mappings corresponding
>>  to all the class constructors as part of the structure, and to
>  > require the universe to be closed under them in an appropriate way.
>>  Call that an OWL structure. Then *independently* say that an OWL
>>  structure satisfies a graph when the graph comes out to be true when
>>  you interpret the OWL vocabulary in the appropriate way. This treats
>>  all the OWL vocabulary as a logical vocabulary, in effect. Right now
>  > we have these two aspects - closure of the universe and satisfaction
>>  of the graph - kind of mixed together. If they were separated then it
>>  would be clearer, I think, that the structures always exist. But
>>  since you and maybe Ian are the only people who need to be convinced
>>  of this, I wonder if its really worth all the trouble....:-)
>>  Actually, a serious point: once the MT gets this complicated, I
>>  wonder if an Lbase-style way of giving the semantics might not be
>>  preferable: its easier to understand, easier to check and just as
>>  formally precise. And it doesnt require us to treat the entire
>>  namespace as logical vocabulary. If SW languages ever get more
>>  complicated than OWL, I wouldnt want to be in the MT business any
>>  more.
>>
>>  >
>>  >[...]
>>  >
>>  >>  >PS:  I would much have preferred to try to get a version of 
>>the previous
>>  >>  >      document that didn't have any known bugs before making 
>>such drastic
>>  >>  >      changes.
>>  >>
>>  >>  Well, the previous approach seemed to be hopeless, and this is really
>>  >>  only a simplified version phrased somewhat differently. The only
>>  >>  major change was realizing that we could impose simplified
>>  >>  restriction closure conditions on large OWL, and let it support all
>>  >>  the intuitive inferences. (That is what took the weekend.)
>>  >
>>  >But this is precisely where I cannot see a way of showing that the model
>>  >theory is non-trivial.
>>
>>  Well, Im not sure what would convince you. One can construct little
>>  interpretations, like the above, to show that it can be done in some
>>  cases; and we all agree that it can't be done in all cases. So where
>>  is your boundary?
>
>Well showing that there was at least one Large OWL interpretation would be
>a good start.  I am definitely not convinced that there is even one.

Actually, I think that is *all* that I need to do. If there is one, 
then your concerns about large OWL/RDFS being uninterpretable are 
clearly unwarranted.

>Showing that a good selection of interesting Large OWL graphs are
>non-contradictory would go almost all the way to convincing me.
>
>It is not as if I am asking for anything special, after all.

I think your insistence on seeing examples rather than accepting a 
general argument is quixotic and wrong-headed, rather like someone 
who doesnt believe that equations have solutions until he is shown a 
few. But I will do my best to convince you.

>  Further, the
>mere fact that I am asking is a bad sign.

I tend to agree, but maybe not about what it is sign of.

Pat

-- 
---------------------------------------------------------------------
IHMC					(850)434 8903   home
40 South Alcaniz St.			(850)202 4416   office
Pensacola,  FL 32501			(850)202 4440   fax
phayes@ai.uwf.edu 
http://www.coginst.uwf.edu/~phayes

Received on Monday, 23 September 2002 22:48:54 UTC