The magic word "definition"

Robert MacGregor <>
Message-id: <>
Subject: The magic word "definition"
Date: Fri, 10 Jan 92 08:44:03 PST
From: Robert MacGregor <>
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