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)
|