ontolog-forum
[Top] [All Lists]

## Re: [ontolog-forum] new logic

 To: "[ontolog-forum]" Christopher Menzel Tue, 19 Jan 2010 17:38:04 -0600 <1263944284.5096.27.camel@new-philebus>
 On Tue, 2010-01-19 at 13:36 -0500, Patrick Cassidy wrote: > John, > Re: Describing a computation with FOL > Can FOL actually *perform* arithmetic functions?    (01) That's like asking whether English can dance the tango. FOL doesn't *do* anything. FOL is a language, a semantics and (typically) a system by means of which an agent can generate proofs. Thus, FOL can be *used* to represent information and demonstrate, e.g., when one thing follows from another. You can therefore *describe* a computation in FOL and prove things about that computation. But FOL of itself doesn't do anything at all.    (02) > 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?    (03) Well, now you've changed the subject from FOL to FOL *reasoning*. And, under one reasonable interpretation of "FOL reasoning", the answer is "yes". For a given Turing machine M halts on input n if and only if there is a corresponding proof in first-order logic that in a precise sense represents M's computation.* Hence, by means of first-order reasoning one can compute a sum, difference, product, ratio etc just as a Turing machine could -- however, typically it would be a lot quicker and easier just to perform a simple arithmetic proof directly using, say, Peano Arithmetic.    (04) Chris Menzel    (05) *This is in fact how one shows that the undecidability of first-order logical implication follows from the halting problem. For details, see Boolos, Burgess, and Jeffrey, Computability and Logic, ch 11.    (06) _________________________________________________________________ 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    (07)
 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 Re: [ontolog-forum] new logic, Paola Di Maio