# conservative definitions

dam@ai.mit.edu (David McAllester)
From: dam@ai.mit.edu (David McAllester)
Date: Mon, 6 Jan 92 21:03:46 EST
Message-id: <9201070203.AA03069@raisin-bran>
To: jmc@cs.stanford.edu
Cc: interlingua@isi.edu
Subject: conservative definitions

I objected to the fact that KIF definitions were not conservative
extensions at the KIF meeting at AAAI-90 a year and a half ago.
It seems to me that the design of KIF is in serious need of input
>From well trained logicians.
Regarding your proposal for extensible definitions --- I think your
proposal works, one just has to be a little careful. Let Phi(x) be a
formula involving one free variable x. There is no difficulty in
working in higher order logic so we can let x range over predicates,
functions, or whatever (as in EKL I think). If we can prove Exists x
Phi(x) then we can introduce a new constant c and assert Phi(c) "by
definition". If we whish to extend this definition by a formula
Psi(x) we need to prove exists x [Phi(x) and Psi(x)]. We can then
assert Psi(c) "by definition extension".
Now consider your problem --- suppose that Phi(x) asserts that x is a
set with certain properties. Further suppose that, given Phi(c) we
can prove Exists y in c Theta(y). The later assertion of Psi(c) is
not in danger of introducing a contradiction. Now matter how we
interpret c as a set such that Phi(c), we must have Exists y in c
Theta(y). If Psi(c) forces c to be a small set then Phi(c) must allow
c to be small and even under this small interpretation of c we must
have Exists y in c Theta(c).
Extendible definitions should probably be called "primitive kinds" and
the term "definition" should be reserved for introducing symbols as
abbreviations for other expressions (such as lambda functions, lambda
predicates, or whatever). Intuitively, a definition should DETERMINE
the meaning of the defined term.
David McAllester