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)