ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Ontological correctness

To: gruninger@xxxxxxxxxxxxxxx
Cc: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Pat Hayes <phayes@xxxxxxx>
Date: Thu, 1 Feb 2007 14:07:33 -0600
Message-id: <p0623090ec1e7f45a0273@[10.100.0.26]>
>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)

<Prev in Thread] Current Thread [Next in Thread>