[Top] [All Lists]

Re: [ontolog-forum] PROF Swartz ON DEFINITIONS

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Mon, 20 Sep 2010 21:55:09 -0400
Message-id: <4C98107D.9030201@xxxxxxxxxxx>
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)

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