ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] PROF Swartz ON DEFINITIONS

 To: ontolog-forum@xxxxxxxxxxxxxxxx "John F. Sowa" Mon, 20 Sep 2010 21:55:09 -0400 <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) ```
 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