Re: Goedel's incompleteness theorom?

On Mar 15, 2007, at 5:41 PM, Daniel J McGoldrick wrote:

> Hello --
>
> I have been following the public-semweb-lifesci discussions
> for some time (silently) with great interest.  By way of  
> introduction, I am the CEO and founder of Sentient Solutions Inc. -  
> a non-profit Colorado company with an affiliated Consulting LLC  
> Sentient Consulting. I worked for UC-computational pharmacology for  
> four years, and for Evolutionary Genomics.
>
> I thought I would chime in for a brief moment. "Sound and  
> Complete"  i.e. consistent and complete is proven impossible by  
> Gödel - see
>
> http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorem
>
> No use wasting time trying to get both in a perfect Panglosian  
> world :-).
[snip]

Except many logics, and I would say nigh all computational logics, do  
have sound and complete proof systems. Indeed, many logics (e.g., OWL  
DL) have *decision procedures*. Among logics with s&c proof  
procedures is first order predicate logic as shown by.....Godel:
	http://en.wikipedia.org/wiki/Gödel's_completeness_theorem

Establishing certain metalogical properties of a formalism does not  
settle the properties of an implementation of that formalism, so  
testing (and other verification techniques) are still required. And,  
of course, if you lack a decision procedure (as with FOL), then there  
are certain answers your implementation won't get, so again care is  
needed. And with expressive decidable logics, the high worst case  
complexity can kill you.

And of course, some times, approximation is good enough. But, in  
general, it's nice to have a formalism that is well behaved,  
computationally and mathematically, and if not computationally, at  
least mathematically, because such formalisms are better understood  
overall.

Cheers,
Bijan.

Received on Friday, 16 March 2007 09:08:50 UTC