On Mar 8, 2007, at 5:01 PM, Pat Hayes wrote:
> ...The notion of
> 'completeness' of a logic or inference machine is
> well-established in logic, used in virtually all
> textbooks, and has a clear, simple definition. It
> means that if X is a logical theorem then a proof
> of X exists, so that a complete inference engine
> is one which will, in principle, find a proof of
> X. (01)
Just a quick clarification to Pat's lucid post: Pat is using
somewhat nonstandard terminology here, as the term "logical theorem"
is usually used to refer to the provable sentences of a logical
system. So understood, that would render Pat's definition trivial
(which is obviously not what he had in mind). The more common term
in the definition of completeness is "logical truth", that is, a
sentence that is true simply in virtue of the meanings of its
component logical operators (or in logician-speak, true under all
interpretations of its nonlogical vocabulary). (02)
Also, the completeness theorem is often stated in a somewhat more
general form whose relevance to formal ontology is a bit clearer: A
logical system (or inference machine) is complete if, for any set of
sentences S (notably, the axioms of an ontology), if S logically
implies X (that is, if X is true under any interpretation that makes
all the members of S true), then there is a proof of X from S. (03)
-chris (04)
_________________________________________________________________
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 (05)
|