ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] new logic

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 19 Jan 2010 17:38:04 -0600
Message-id: <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)

<Prev in Thread] Current Thread [Next in Thread>