definitions and analytic truth
John McCarthy <jmc@sail.stanford.edu>
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.