[Top] [All Lists]

Re: [ontolog-forum] new logic

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Tue, 19 Jan 2010 10:57:50 -0500
Message-id: <4B55D67E.30200@xxxxxxxxxxx>
Rob,    (01)

I'll admit that the word 'described' could be interpreted in
more than one way.  But the interpretation I intended makes
the following statement uncontroversial:    (02)

JFS>> In fact, every program on every digital computer can be
 > described in FOL.  Most aren't, but the machine itself and
 > everything that runs on it can, in principle, be defined
 > in FOL.    (03)

RF> This does seem a very strong statement.    (04)

The proof follows directly from elementary comp. sci.:    (05)

  1. Every digital computer and every digital device attached
     to it (such as I/O devices or graphics engines) can be
     simulated by a Turing machine (TM), which computes exactly
     the same results as the original device, but more slowly.    (06)

  2. Anything computable by one of more TMs working together
     can be simulated by a single TM that can compute the same
     results as the original collection of TMs but more slowly.    (07)

  3. Every TM can be defined by a finite, but extendible string
     of symbols called a *tape*, a pointer to one symbol somewhere
     on that tape, and a set of axioms in FOL that specifies how
     the current symbol is modified and how the pointer moves to
     another symbol.    (08)

This is what I had intended by the term 'describes'.    (09)

RF> Is it not true that a lot of what we might regard as
 > "meaningful" about some programs, such as whether they
 > will ever halt, will escape any such description?    (010)

Those descriptions go beyond the original specification,
but many of them can also be described in FOL.  In fact,
the predicate Will_Halt(M,T), which states whether or not
machine M will halt given tape T, can be defined in FOL.    (011)

For some pairs of (M,T), the predicate Will_Halt can be
determined by a proof in FOL.  But for others, the theorem
prover will loop forever.  But any (M,T) that is undecidable
in FOL will be just as undecidable in English or any other
language, formal or informal.    (012)

There is, of course, an enormous amount of verbiage that has
been written about computers and programs.  Much of it goes
far beyond FOL, and much of the rest would lose a great deal
of the intended meaning if translated to FOL.    (013)

For examples, see the translation of Windows error messages
to haiku, which add that certain "je ne sais quoi":    (014)

    http://www.crisbrady.net/WinHaiku.html    (015)

John    (016)

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

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