The magic word "definition"

• Mail folder: Interlingua Mail
• Next message: schubert@cs.rochester.edu: "Re: Primitives, definitions, and metalanguage"
• Previous message: sowa@watson.ibm.com: "Need for standards"

Message-id: <9201101644.AA21129@quark.isi.edu>
To: interlingua@isi.edu
Reply-To: macgregor@isi.edu
Subject: The magic word "definition"
Date: Fri, 10 Jan 92 08:44:03 PST
From: Robert MacGregor <macgreg@isi.edu>

JS is providing additional fuel for my point about definitions.

> ... you define A as B and define B as C.  Then both of the following
> statements are true in the metalanguage:
> 
>    A is defined as B.
>    B is defined as C.
> 
> But the following statements in the metalanguage are false:
> 
>    A is defined as C.
>    B is defined as A.
>    C is defined as B.
>    C is defined as A.
> 
> However, because of the two definitions above, all six of the following
> equations are true in the object language:
> 
>    A = B.  B = A.  A = C.  C = A.  B = C.  C = B.

This is my point about symmetric operators (in this case "=").
You can't come up with a semantics for definitions without introducing
"something more" than just what the = or <=> operator tells you.

> It only becomes a definition
> when you add that magic metalinguistic word "definition":
> 
>    Definition:  A = (lambda x)B(x).

Correct, but this has to be translated into something that
means something, since "Definition:  A = (lambda x)B(x)"
is not a valid KIF expression.  My purpose in inventing the
definition relation, e.g.,
   (definition A '(lambda x)B(X))
was to add that extra something.

- Bob