[Top] [All Lists]

Re: [ontolog-forum] Form and content

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Sat, 12 Dec 2009 20:40:24 -0500
Message-id: <4B244608.9000308@xxxxxxxxxxx>
Adrian,    (01)

I assume that you wrote that statement in a moment of weakness.
It is not a claim that any competent computer scientist would make:    (02)

AW> So my point is that a useful Logic (or other description method)
 > including the integers should be designed to be as expressive as
 > possible, while stopping short of undecidability.    (03)

I will agree that there are good reasons for certain kinds of
restrictions on languages for special purposes (e.g., Horn clause).
I also agree that language designers should take a course in
computability and decidability.  But blanket statements such as
the above are not merely false.  They are extremely misleading.    (04)

Every major programming language has the ability to express algorithms
that are undecidable.  Yet even algorithms that are undecidable on
some data can be valuable for those inputs on which they terminate.    (05)

For example, every theorem prover for full first-order logic will
fail to terminate on some very complex statements.  But all the
theorems in FOL that Whitehead and Russell published in the
_Principia Mathematica_ can be proved in a fraction of a second
with modern theorem provers.    (06)

Furthermore, it is extremely unlikely that a nonmathematician
could write an undecidable FOL statement.  The Cyc language,
for example, uses a superset of FOL, but knowledge engineers
have rarely, if ever, written an undecidable statement in Cyc.
They wrote many that were false or buggy, but undecidability
was *never* a serious problem for Cyc.    (07)

Even a statement S that is undecidable as a theorem can still be
used in other ways that are easily decidable.  For example, S
could also be used as a query:    (08)

    Is S true of the database D?    (09)

SQL has the full expressive power of FOL, and it's possible to
take an unprovable statement such as S, translate it to an SQL
WHERE-clause, and answer the above query in polynomial time.    (010)

In recent years, an incredible amount of nonsense has been
written about expressive power and decidability.  I wrote
the following paper to clarify some of those issues:    (011)

    Fads and Fallacies about Logic    (012)

John    (013)

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
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (014)

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