[Top] [All Lists]

Re: [ontolog-forum] Logic, Datalog and SQL

To: "[ontolog-forum] " <ontolog-forum@xxxxxxxxxxxxxxxx>, Christopher Menzel <cmenzel@xxxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Kathryn Blackmond Laskey <klaskey@xxxxxxx>
Date: Mon, 12 Feb 2007 08:25:10 -0500
Message-id: <p0611042dc1f6154223a0@[]>

>Following is a revised version:
>     A formal ontology consists of a theory T stated in
>     some version of logic and a nonempty vocabulary V
>     of types and relations.  The names in V are divided
>     in three disjoint subsets:
>     1. Names defined elsewhere, which are used in one
>        or more axioms of T.
>     2. Names defined in T, which may be used in other
>        theories.
>     3. Names that are never used in any other theories.
>     To be considered an ontology, the set of names in
>     subset #2 must be nonempty; i.e., the theory T
>     must define one or more types or relations, whose
>     names may be used in statements other than T.
>    (01)

Enderton defines a theory as a set of sentences closed under logical 
implication.    (02)

I am willing to say that for any any formal ontology (formalized in a 
logic with Boolean truth-values) there exists a smallest set (often 
infinite and often not recursively enumerable) of sentences closed 
under logical implication, which I'll call the theory for the 
ontology.  I'm willing to call any two ontologies equivalent if they 
are in the same equivalence class under the relation "has the same 
theory as".  But I'm a little queasy about identifying the ontology 
with the set of sentences closed under logical implication.    (03)

When I define a formal ontology, I am -- if I've taken a course in 
logic -- aware that I have implicitly specified a smallest set of 
sentences that is closed under logical implication.  But it seems to 
do violence to the notion of an ontology as a formalization of 
knowledge about a domain to say that the ontology IS that (possibly 
infinite) set of sentences.  I may "know" the axioms, but there 
doesn't seem to be any reasonable sense in which I "know" the 
infinite set of sentences.  We need theorem provers because we DON'T 
"know" all the logical consequences of a set of axioms.  Furthermore, 
if the theory is strong enough to axiomatize arithmetic, there are 
undecidable sentences -- sentences whose truth-value will never be 
established in finite time by any theorem prover.    (04)

Kathy    (05)

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    (06)

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