Re: Definitions and analytic truth

• Mail folder: Interlingua Mail
• Next message: David McAllester: "conservative definitions"
• Previous message: sowa@watson.ibm.com: "Existence proofs for defined terms"
• In-reply-to: sowa@watson.ibm.com: "Definitions and analytic truth"
• Reply: John McCarthy: "Definitions and analytic truth"

Date: Mon, 6 Jan 1992 13:57:03 PST
From: Richard Fikes <fikes@sumex-aim.stanford.edu>
Subject: Re: Definitions and analytic truth
To: jmc@cs.stanford.edu
Cc: interlingua@isi.edu, sowa@watson.ibm.com
In-reply-to: Your message of Mon, 6 Jan 92 11:39:15 EST
Message-id: <MacMS.4271.5627.fikes@sumex-aim.stanford.edu>

> All this is rather complicated, so I'm still not sure whether the
> word "definition" is being used in the sense of mathematical logic
> as a sentence that introduces a constant symbol in a conservative
> way.  If not, then you should choose another word instead of
> "definition", because definitions in the sense of mathematical
> logic will surely be required.

John,

I'm not sure I understand the notion of "_conservative_ extension" well enough
to determine whether and in what ways KIF definitions violate that notion. 
Specifics in that regard from you would be helpful.  It is the intention of
KIF definitions (as I understand them) to be used to introduce new constant
symbols, as follows.  KIF has four syntactic forms for definitions:

For defining function constants:

  (defunction <name> (<indvar>* [<seqvar>]) <term>)

For defining relation constants:

  (defrelation <name> (<indvar>* [<seqvar>]) <sentence>*)
  (defprimrelation <name> (<indvar>* [<seqvar>]) <sentence>*)

For defining object constants:

  (defobject <name> <sentence>*)


The domain assertion associated with a definition is the sentence that can be
considered to be true "by definition" from the definition.  The proposal I
described last evening is for the domain assertions for each form to be as
follows:

For (defunction <name> (<indvar>* [<seqvar>]) <term>):

   (= <name> (lambda (<indvar>* [<seqvar>]) <term>))

For (defrelation <name> (<indvar>* [<seqvar>]) <sentence>*):

   (= <name> (kappa (<indvar>* [<seqvar>]) (and <sentence>*)))

For (defprimrelation <name> (<indvar>* [<seqvar>]) <sentence>*):

   (=> (<name> @args) ((kappa (<indvar>* [<seqvar>]) (and <sentence>*))
@args))

For (defobject <name> <sentence>*)

   (and <sentence>*)


The defobject form seems to be the only one that could introduce arbitrary
sentences as definitional.  What would we need to do to prevent that?  Require
that each sentence (conjunct?  disjunct?) contain an occurrence of the
constant being defined?

One way of assuring that arbitrary sentences cannot be definitions (if that is
what we want) is to change defobject to the following more restrictive form:

    (defobject <name> <term>)

with the following domain assertion:

    (= <name> <term>)

But then, we would have no way of defining an object constant by specifying a
set of (definitional) axioms about it.  What do you think?

Richard




-------