John,
Re: Describing a computation with FOL
Can FOL actually *perform* arithmetic functions?
I know that one can assert that there is a function that takes two
numbers and associates with them their sum, but it seems that to use such a
function in FOL one needs to have a preexisting table of such sums,
impractical in the general case.
Is there a way for FOL reasoning to actually **compute** a sum (or
difference, product, ratio) as a Turing machine could? An example would be
instructive. (01)
Pat (02)
Patrick Cassidy
MICRA, Inc.
908-561-3416
cell: 908-565-4053
cassidy@xxxxxxxxx (03)
> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
> bounces@xxxxxxxxxxxxxxxx] On Behalf Of John F. Sowa
> Sent: Tuesday, January 19, 2010 10:58 AM
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] new logic
>
> Rob,
>
> 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:
>
> 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.
>
> RF> This does seem a very strong statement.
>
> The proof follows directly from elementary comp. sci.:
>
> 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.
>
> 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.
>
> 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.
>
> This is what I had intended by the term 'describes'.
>
> 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?
>
> 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.
>
> 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.
>
> 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.
>
> For examples, see the translation of Windows error messages
> to haiku, which add that certain "je ne sais quoi":
>
> http://www.crisbrady.net/WinHaiku.html
>
> John
>
>
> _________________________________________________________________
> 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
> (04)
_________________________________________________________________
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 (05)
|