ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] PROF Swartz ON DEFINITIONS

 To: "[ontolog-forum]" Alex Shkotin Wed, 22 Sep 2010 18:56:27 +0400
 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+2andplusTwo(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;-)Alex2010/9/21 John F. Sowa 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) ```
 Current Thread [ontolog-forum] PROF Swartz ON DEFINITIONS, FERENC KOVACS Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Peter Yim Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Rich Cooper Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Alex Shkotin Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, doug foxvog Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Rich Cooper Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Alex Shkotin Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Christopher Menzel Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, John F. Sowa Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Alex Shkotin <= Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, John F. Sowa Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Christopher Menzel Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, John F. Sowa Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Patrick Durusau Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Christopher Menzel Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, Alex Shkotin Re: [ontolog-forum] PROF Swartz ON DEFINITIONS, FERENC KOVACS