>Hi Pat,
>
>Quoting Pat Hayes <phayes@xxxxxxx>:
>
>> Michael Gruninger <mudcat@xxxxxxxxxxxxxxx> wrote:
>
>> >An ontology will be complete with respect to these intended structures if
>> >all of the models of the axioms are isomorphic (or
>> >possibly elementarily equivalent)
>> >to the intended structures.
>>
>> I agree this is very nice definition of
>> correctness and completeness, the straight
>> model-theoretic view. Unfortunately, though, it
>> doesn't seem (to me) to be very useful in
>> practice, for several reasons. First, this kind
>> of completeness is almost never obtainable,
>> because of Goedel: you can't even get it for
>> arithmetic.
>
>This is vastly overstating the case -- there is more to life than PA. (01)
True, but most 'real-life'; ontologies take the integers for granted
e.g. anything in RDFS or OWL assumes that the XSD datatypes, which
include 'number', are given; and the semantic specification for XSD
seems to require that all interpretations of that datatype are
*standard* models of the integers; although I concede that might not
be what the authors of the spec. intended. (02)
>In fact, there are many theories for which we can prove completeness. (03)
In isolation, i.e. for that theory taken alone. But in an 'open'
context like the Web such closure cannot be assumed. (04)
>In terms of real ontologies, this approach has been successfully
>done with all of the core theories of the PSL Ontology, (05)
Can you point me at where this is written up? Im interested to see
what the proof strategy is to establish isomorphism. (06)
> and is
>almost done for the remaining definitional extensions of
>that ontology. It has been done for a first-order axiomatization
>of a computer vision domain for 2D object recognition. (07)
Ditto. (08)
>It has been done for several ontologies in the domain of mereotopology. (09)
Ditto, though there the idea seems more plausible, I agree. (010)
It is interesting, I have found attention to models more use to show
incorrectness/incompleteness, by exhibiting satisfying
interpretations which clearly fail to be 'intended' models of the
domain under consideration. (I learned this trick from Johan van
Bentham.) So in the 'time catalog' for example its often not hard to
give clearly 'nonstandard' models of many temporal ontologies, and
this is often very useful as a way of pinpointing gaps and
weaknesses. For example, no amount of axiomatic chuntering about time
ordering is going to prevent your theory having models in which all
of time fits in the unit interval. Moral: to really capture the idea
of 'a very long time', you have to talk about durations. (011)
>I'm not denying that there exist classes of structures that cannot
>be axiomatized, or that any ontology containing PA is incomplete.
>Nevertheless, as said in my earlier reply to Chris M., we often take the
>easy route and use PA to axiomatize concepts that we could have
>actually axiomatized with a weaker theory. (012)
Well, that is a reasonable point, indeed. We should always be on the
lookout for plausible weakenings. (013)
>
>> Second, even if we abandon
>> completeness, its about as hard (harder?) to
>> describe the class of intended models as it is to
>> state the facts using the formal language itself.
>
>If you can't formalize your intuitions, what axioms
>are you writing? Once you have written your axioms,
>you still need to characterize the models of these axioms. (014)
Im not sure I agree. Its often useful, but why do you HAVE to? Why
isn't it enough to simply say, the models are all the models of my
axioms. (And I havn't got any better way to characterize them.) Do
you have a better way to characterize models of, say, Peano
arithmetic? When we were writing the RDF semantics, it was often a
toss-up whether to specify things in model-theoretic terms or just to
list a lot of 'obvious' axioms and say, an RDFS interpretation is
anything that satisfies all of these. We were scolded by some
theoreticians, but most people found it far easier to understand the
second approach (and far more use, since they could type the axioms
into their reasoners and use them directly.) (015)
Seems to me that one of the great merits of the completeness theorem
is that it gives you this methodological freedom. (016)
>Once you have this characterization up to isomorphism,
>you can then look through these models to see if they all
>make sense (i.e., they are all intended). If they are not,
>you add axioms to remove the unintended ones. (017)
Right, that's a good strategy I agree. But you don't need a COMPLETE
survey to do this. (018)
>If you can't add axioms (i.e. there are continuum many
>unintended models, as with PA), well, then we can give up,
>and we will need to be satisfied with correctness and not completeness.
>
>
>> The relational structrures will look very
>> different (though there are of course mappings
>> between them) but they can both be 'fitted' onto
>> the actual weather, one presumes, but 'fitted'
>> differently.
>>
>> In a nutshell: reality isn't a relational
>> structure. One can hallucinate a relational
>> structure onto it in many different ways. Which
>> of *these* is "right"? Does the question even
>> make sense?
>
>I am not some wild-eyed Platonist who thinks that
>there is One True structure for reality. (019)
:-) Funny, Im not a Platonist either, but I actually DO think there
is one true structure of reality. (I refuse to defend this position
on this list.) (020)
>When it comes to ontology design and evaluation,
>I am a pragmatist. (021)
Me too, though I agree with Matthew about elegance and economy (022)
>By the soundness and completeness of first-order logic,
>there is a nice side-effect of showing that your ontology
>axiomatizes the class of intended models -- any sentence
>satisfied by all models will be derivable from the axioms.
>You will have the "right" models if you can derive the
>"right" consequences from the axioms. (023)
True, though that kind of begs the question, right? (024)
>What are the "right" consequences?
>That's the question for the ontology designer. (025)
Which is where I came in. (026)
Pat
--
---------------------------------------------------------------------
IHMC (850)434 8903 or (650)494 3973 home
40 South Alcaniz St. (850)202 4416 office
Pensacola (850)202 4440 fax
FL 32502 (850)291 0667 cell
phayesAT-SIGNihmc.us http://www.ihmc.us/users/phayes (027)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (028)
|