On 9/20/2010 1:23 PM, Christopher Menzel wrote:
> Actually, recursive definitions are not proper definitions in FOL, so
> the "=_df " is in fact misplaced here (Prof Swartz's use of the notation
> notwithstanding). In a genuine definition, the defined term is in a
> certain (rigorous) sense dispensable; it is a convenience that one
> could, in principle, do without. Unlike a recursive definition, then,
> in a genuine definition, the defined expression cannot occur in the
> definiens. (01)
I agree. But I'd just like to add a few comments. (02)
Pat Hayes noted that the CL standard does not have any notation
that uses the term 'definition' or 'def' or anything similar. (03)
However, the effect of a definition can be obtained by using
the operator 'iff' (an abbreviation of 'if and only if') to
state that two sentences are true or false under exactly the
same conditions. I could also use the operator '=' to say
that two functions have the same value for any arguments. (04)
For example, suppose that somebody has written axioms to specify
a function named '+' that takes two numbers as arguments to
produce another number as the result. (05)
Then I might decide to define a function called 'plusTwo'
in terms of the '+' function: (06)
(forall (x)
(= (plusTwo x) (+ x 2))) (07)
This is called a *closed form* definition because it allows
any occurrence of the expression (plusTwo x) to be replaced
by the expression (+ x 2), which is a "closed form". (08)
But as Chris noted, a recursive definition does not
correspond to any closed form expression. (09)
In fact, it might not be a definition if the recursion would
run forever without stopping with a unique result. (010)
Before it could be considered a definition, one would have
to prove a theorem to show that the recursion would stop with
a unique result for any value of the input argument(s). (011)
John (012)
_________________________________________________________________
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 (013)
|