ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] new logic

 To: "'[ontolog-forum] '" "Patrick Cassidy" Tue, 19 Jan 2010 13:36:03 -0500 <001401ca9936\$4178f410\$c46adc30\$@com>
 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)
 Current Thread Re: [ontolog-forum] new logic, Rob Freeman Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Patrick Cassidy <= Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Adrian Walker Re: [ontolog-forum] new logic, Christopher Menzel Re: [ontolog-forum] new logic, Patrick Cassidy Re: [ontolog-forum] new logic, Jakub Kotowski Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Patrick Cassidy Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Rich Cooper Re: [ontolog-forum] new logic, Rob Freeman