**Mail folder:**Interlingua Mail**Next message:**sowa@watson.ibm.com: "Definitions and analytic truth"**Previous message:**sowa@watson.ibm.com: "Resolution of SQL debate"**In-reply-to:**schubert@cs.rochester.edu: "definitions and analytic truth"**Reply:**sowa@watson.ibm.com: "Definitions and analytic truth"

Date: Fri, 3 Jan 92 16:38:32 -0800 From: John McCarthy <jmc@sail.stanford.edu> Message-id: <9201040038.AA10435@SAIL.Stanford.EDU> To: schubert@cs.rochester.edu Cc: interlingua@isi.edu, saraswat@parc.xerox.com, sowa@watson.ibm.com In-reply-to: schubert@cs.rochester.edu's message of Fri, 3 Jan 92 18:45:04 EST <9201032345.AA02348@ash.cs.rochester.edu> Subject: definitions and analytic truth Reply-To: jmc@cs.stanford.edu

It seems to me that KIF definitions should be _conservative_ extensions of the language just as definitions are in logic. One should not be able to sneak in a new assertion in the guise of a definition. Jussi Ketonen's EKL interactive theorem prover handles it is follows. Let foo be a new symbol and P{foo} any formula containing foo. Provided one can prove (exists foo)P{foo}, one can write P{foo} giving "by definition of foo" as the reason. The easiest case of this is when P{foo} has the form foo = rhs, where rhs does not contain foo. Of course, P{foo} could also be (all x y z)(foo(x,y,z) iff rhs), where again rhs does not contain foo. The use of definition can make arguments shorter, but in first order logic and, I believe, the higher order logic of EKL, definitions don't allow any formula not containing the defined term defined to be proved that isn't provable without the definition. Since KIF allows nonmonotonic reasoning, the inference of (exists foo)P{foo} may be nonmonotonic also. This method of definition is essentially one of partial definition, since one is not required to infer that there is a unique foo satisfying P{foo}. We can also achieve the successive refinement of a definition by adding just a little syntactic sugar to the previous notion. Suppose foo has already been defined. Then our previous method allows defining a new symbol baz by the formula P{baz} taking the form baz = foo and P1{baz}, where P1{baz} gives the new desired properties. We still have to infer P{baz}. No this isn't correct, because that would would require proving P{baz}, where foo is any entity satisfying P{foo}, whereas we want merely to have to show that there is an entity foo satisfying P{foo} and P1{foo}. Doubtless this can be fixed up. Anyway the main point is that one simple mechanism gives all one can ask for in definitions given that definitions should be conservative extensions and not disguised new axioms.