The magic word "definition"Robert MacGregor <firstname.lastname@example.org>
Subject: The magic word "definition"
Date: Fri, 10 Jan 92 08:44:03 PST
From: Robert MacGregor <email@example.com>
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.