ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] Constructs, primitives, terms

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: William Frank <williamf.frank@xxxxxxxxx>
Date: Thu, 8 Mar 2012 15:04:31 -0500
Message-id: <CALuUwtABmT2ocLcpcoetB=3qc6VY2056M738P9cKqtv344usRQ@xxxxxxxxxxxxxx>


On Thu, Mar 8, 2012 at 1:32 PM, Christopher Menzel <cmenzel@xxxxxxxx> wrote:
Am Mar 8, 2012 um 6:23 PM schrieb William Frank:
> I think is the essence of this point is:
>
> "The number of possible conflicts is infinite, and no fixed set
> of universal definitions can anticipate and rule out all of them."
>
> This is true of *logical necessity*; so it is something that we always live with
>
> The reason for this truth is that
>
> there is no guarantee that all the models for
> any theory G are consistent with one another.

I not sure what you and John mean by that -- consistency is a property of theories or, more generally, sets of sentences. It doesn't make any clear sense that I can see to say that two models are inconsistent. I suppose we can make something up, e.g., models M1 and M2 of theory G are inconsistent with each other if there is some sentence A in the language of G (obviously not a theorem of G) to which M1 and M2 assign different truth values.

Actually, I was making something up to save words, that seemed clear, indeed only theories can be consistent or otherwise, two models are inconsistent if there are two theories of which they are models, which are inconsistent. 


> More strongly, unless the theory G is complete, which no theory as expressed in an application will be

It's not obvious to me that that is so. There are well-known examples of complete first-order theories (e.g., the first-order real number theory and Euclidean geometry both have complete axiomatizations). Such theories obviously cannot contain a lot of arithmetic, but it's not obvious that an interesting practical ontology has to contain the arithmetic needed to guarantee incompleteness and hence can't be complete.

Well, what I had in mind is ontologies for things like trade services or pharmaceuticals. These seem alot more complex to me than geometry etc.  As many in these exchanges have noted, most large software collections are probably  inconsistent, but consistency is to be hoped for.  To expect one of them to be complete is a stretch, and probably not desireable. 

> (only theories as bounded and richly expressed as second order arithmetic tend to be complete),

Eh? There is no complete axiomatization of second-order arithmetic.

Sorry, I was not clear. There are two meanings of complete floating around.  I was using semantic completeness, in the model theory semantically complete sense, as used by Baldwin "what is a complete theory?"

"
A (consistent) theory T in a logic L is complete if for every
L-sentence ,
T |= L
or
T |= ¬ L. 
"

where the sideways sleepy |= means logically follows from, not is provable from.

As opposed to the completeness of a proof theory, which means as you say, if it follows, then you can prove it.

The term "completeness," as it applies to a  logic, I believe, is only as you define it. As it applies to a contentful theory expressed in a logic, I believe it usually means what I an Baldwin mean.
Second order arithmetic is sematincally complete while it is proof theoretically incomplete, since second order logic itself is proof-theory  incomplete.

> there will always be models, describe in theories G' that are extensions of G, as expressed in different applications, that ARE inconsistent with each other. As in John's example, "an employee must be at least 21 years of age," may be a rule expressed in one applicaton, while in another employees may be 16, or have no specified age limits.

OK, so if you've got a theory G that doesn't entail anything specific about age limits, then you could extend G to theories G1 and G2 that specify different age limits. Hence, a model M1 of G1 and a model M2 of G2 will both be models of G but will be "inconsistent" in the sense above. Fine, but it seems to me this is all more easily expressed proof theoretically -- it's the simple logical fact that every consistent incomplete theory has consistent extensions that are mutually inconsistent.

you are right, that might be an easier way to say it, especially if you expand out all my lazy ellipses.  Or else completely (no pun intended) on the model theoretic side.  Mixing the two together is generally a more complex thought to follow. 

The point remains, which was the point of the mail:  ontologies do not guarantee complete "interoperability", but that term probably needs and does not have a definition.  And if ontologies only guarantee something partial, what is it that they DO guarantee?  And why, in practice, do even primitive but logical shared messaging specifications like the early tagged syntax S.W.I.F.T provide so much value, and not seem to lead us into trouble.  (While some shared but literally insane messaging specification like the health care EDI messages create huge error and correspondingly huge employment opportunities

-chris



_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J




--
William Frank

413/376-8167


This email is confidential and proprietary, intended for its addressees only.
It may not be distributed to non-addressees, nor its contents divulged,
without the permission of the sender.

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: 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 join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

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