ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] new logic

 To: "[ontolog-forum]" Jakub Kotowski Wed, 20 Jan 2010 09:15:03 +0100 <4B56BB87.4010409@xxxxxxx>
 Hello Patrick,    (01) Patrick Cassidy wrote: > Naively, I would be curious to see how the function "plus" would be > described in FOL so that for any two arbitrary integers n and m, the sum > (plus n m) could be evaluated by FOL reasoning over the set of axioms > describing the "plus" function. > Is this described somewhere in a form that non-mathematicians could > understand?    (02) I think the Peano axioms are what you are looking for: http://en.wikipedia.org/wiki/Peano_axioms    (03) To summarize, the "trick" is to have a unary representation of natural numbers using a constant symbol 0 and a successor function S. Then 1 is S(0), 2 is S(S(0)), ...    (04) Then after axiomatizing the equality relation and properties of natural number, the plus function can be recursively defined as:    (05) a + 0 = a a + S(b) = S(a + b)    (06) Jakub    (07) > > Pat > > Patrick Cassidy > MICRA, Inc. > 908-561-3416 > cell: 908-565-4053 > cassidy@xxxxxxxxx > > >> -----Original Message----- >> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum- >> bounces@xxxxxxxxxxxxxxxx] On Behalf Of Christopher Menzel >> Sent: Tuesday, January 19, 2010 6:38 PM >> To: [ontolog-forum] >> Subject: Re: [ontolog-forum] new logic >> >> 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? >> 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. >> >>> 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? >> 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. >> >> Chris Menzel >> >> *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. >> >> >> >> >> _________________________________________________________________ >> 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 >> > > > _________________________________________________________________ > 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 > >    (08) _________________________________________________________________ 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    (09)
 Current Thread Re: [ontolog-forum] new logic, (continued) 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 Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, Paola Di Maio Re: [ontolog-forum] new logic, John F. Sowa Re: [ontolog-forum] new logic, ravi sharma