Chris,
Thanks for the elaboration. But I don't have time to delve into proof
theory, I would be quite satisfied to see an actual demonstration of an FOL
specification that showed how a "plus" function could be described in a
general way so that any arbitrary number can be added to any other. I can
visualize (I think) a set of axioms that would describe what the sum of two
integers would be, and how to carry over a 1 to the next decimal place, but
my simple imaginings rely on having some upper limit to the number of places
that the axioms could handle, so that the carryings would only succeed as
far as they were explicitly mentioned in the axioms. I suppose from what
you say, this can be generalized, but rather than try to figure it out with
my limited math background, it would be nice to see such an axiomatization
of arithmetic in FOL.
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? (01)
Pat (02)
Patrick Cassidy
MICRA, Inc.
908-561-3416
cell: 908-565-4053
cassidy@xxxxxxxxx (03)
> -----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
> (04)
_________________________________________________________________
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 (05)
|