ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] new logic

 To: "[ontolog-forum]" Christopher Menzel Tue, 19 Jan 2010 11:40:00 -0600 <4B55EE70.5000500@xxxxxxxx>
 ```On 1/19/2010 9:57 AM, John F. Sowa wrote: > 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'.    (01) Even more abstractly still, a TM can simply be /identified /with its program, a finite set of (typically) 4-tuples. One can then define, for any TM, a precise notion of a *run* of that TM on any given input (i.e., on any given initial "tape"), that is, a precise notion of how the program alters the initial input step-by-step. Mathematically, the initial input, i.e., a tape, is nothing but a sequence (in the mathematical sense) of symbols and a run is jut a sequence of such sequences. All of this is easily definable in first-order set theory. See, e.g., Davis, Sigal, and Weyuker, /Computability, Complexity, and Languages/.    (02) > 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.    (03) They can *all* be described in FOL.    (04) > 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.    (05) Yes, it is the simple statement, translated into FOL, that, for some natural number n, the length of the run of M on tape T is n.    (06) > 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.    (07) Right, whether or not we can PROVE that a given TM will halt on a given input is an entirely different question, one that has nothing to do with first-order logic /per se/.    (08) Chris Menzel    (09) _________________________________________________________________ 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    (010) ```
 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