[Top] [All Lists]

Re: [ontolog-forum] formal systems, common logic and lbase

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Sun, 18 Nov 2007 12:59:53 -0500
Message-id: <47407D99.7040400@xxxxxxxxxxx>
Rick,    (01)

Thanks for the reference.  Soloman Feferman is a very good logician,
who edited Gödel's _Collected Papers_, and his views are well taken.    (02)

But the question about the potential of human minds vs. computer
programs is extremely complex, and I'd like to mention one commonly
claimed, but erroneous argument:    (03)

  1. Gödel proved that there are infinitely many true theorems that
     cannot be proved by a machine that enumerates all proofs.    (04)

  2. But humans can prove some theorems that are outside some list
     of enumerated proofs.    (05)

  3. Therefore, humans can do things that no machine ever could.    (06)

The point to note is that humans can't enumerate all proofs any
better (in fact much worse) than a computer.  What they have done
to "cherry pick" the low-hanging fruit.  To be specific, they have
found some examples of true statements that are outside a certain
list of theorems.    (07)

But it's also possible for a computer to "cherry pick" simple
theorems that happen to lie outside a given enumeration.  So
that argument and many others, which may be disguised by side
issues about neurons and quantum mechanics, prove nothing.    (08)

In any case, it is quite obvious that people don't think like
computers.  The neatly formalized proofs in mathematical
journals have no resemblance to the way the authors actually
discovered them.  See the quotations below.    (09)

 > Seems to me that efforts like Common Logic and LBase would either
 > have to a) be defined within this type of an open ended system,
 > let's say as the natural language description of the constraints
 > to which the axioms that make up the theory of such a system
 > would  adhere; or b) evolve into an open ended system that
 > exhibits characteristics of transformation across languages,
 > logics, models and theories.    (010)

I strongly agree that we have to keep our systems open ended.
But Common Logic and the LBase subset are neutral with respect
to the methodologies for designing and using open-ended tools
and ontologies.    (011)

Common Logic is a generalization of a wide range of logic-based
tools and systems that have been developed over the past 30
years, and it can support many more systems and methodologies.    (012)

There have also been some requests for more features, which
have been included in the IKL proposal.  There are still many
questions about which extensions should be included in a future
version of CL, but they can be considered as time goes by.    (013)

___________________________________________________________________    (014)

Paul Halmos, mathematician:    (015)

     Mathematics — this may surprise or shock some — is never deductive 
in its creation. The mathematician at work makes vague guesses, 
visualizes broad generalizations, and jumps to unwarranted conclusions. 
He arranges and rearranges his ideas, and becomes convinced of their 
truth long before he can write down a logical proof... the deductive 
stage, writing the results down, and writing its rigorous proof are 
relatively trivial once the real insight arrives; it is more the 
draftsman's work not the architect's.    (016)

Richard Feynman, physicist:    (017)

     We have a habit in writing articles published in scientific 
journals to make the work as finished as possible, to cover up all the 
tracks, to not worry about the blind alleys or describe how you had the 
wrong idea first, and so on. So there isn't any place to publish, in a 
dignified manner, what you actually did in order to get to do the work.    (018)

Gian-Carlo Rota, mathematician:    (019)

     Shocking as it may be to a conservative logician, the day will come 
when currently vague concepts such as motivation and purpose will be 
made formal and accepted as constituents of a revamped logic, where they 
will at last be alloted the equal status they deserve, side-by-side with 
axioms and theorems.    (020)

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

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