Re: [ontolog-forum] PROF Swartz ON DEFINITIONS

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

John,

definition is very important for understanding and education of a mind.
Eliminate from theory all "*closed form* definition" and I do not get any idea about practically any theorem. 

From other side just compare 

plusTwo(x) = x+2

and

plusTwo(x) = (x+2)+(x-x)

the second is not a definition (I hope).

If we have a concept in mind or a term in language it is very important question - what is its definition?

Or even, do it have definition at all? 
Or, what kind of theory do we need to have definition for example for biological species?

And it is true that these definitions may be embedded in CL for derivation and other needs.
But not before we get them;-)

Alex

2010/9/21 John F. Sowa <sowa@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.

I agree.  But I'd just like to add a few comments.

Pat Hayes noted that the CL standard does not have any notation
that uses the term 'definition' or 'def' or anything similar.

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.

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.

Then I might decide to define a function called 'plusTwo'
in terms of the '+' function:

   (forall (x)
      (= (plusTwo x) (+ x 2)))

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".

But as Chris noted, a recursive definition does not
correspond to any closed form _expression_.

In fact, it might not be a definition if the recursion would
run forever without stopping with a unique result.

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).

John

_________________________________________________________________
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)