Re: [ontolog-forum] new logic

[Adrian Walker <adriandwalker@xxxxxxxxx>]

Hi Chris --

You wrote..

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.

Yes indeed, FOL plus an inference engine can do (integer) arithmetic.  

However, in all of the practical logic-based systems I'm aware of, arithmetic is actually done by "built in predicates", aka calls to traditional libraries coded in C, Java or such.

                           Cheers,  -- Adrian

Internet Business Logic
A Wiki and SOA Endpoint for Executable Open Vocabulary English over SQL and RDF
Online at www.reengineeringllc.com    Shared use is free, and there are no advertisements

Adrian Walker
Reengineering

On Tue, Jan 19, 2010 at 6:38 PM, Christopher Menzel <cmenzel@xxxxxxxx> wrote:

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