Definitions and analytic email@example.com
Date: Fri, 3 Jan 92 12:14:43 EST
Subject: Definitions and analytic truth
I agree with Bob MacGregor that lambda expressions should be the
normal means for stating definitions: a function symbol is simply
a synonym for the lambda expression that defines it. There might
also be some primitive functions that have no definitions. In that
case, their behavior would be determined by a set of axioms or laws.
I also find the "analytic-truth" predicate very distasteful. Presumably,
it means that the assertion is provable from some set of laws. But in
that case, there is a missing argument -- namely, which laws?
There are some very serious philosophical arguments about the distinction
between analytic and synthetic (see for example, Quine's _Word and
Object_). I think we should avoid using terms that are so highly charged
with philosophical controversy. If we say, instead, that there are named
contexts, each with its own set of laws, then the "analytic-truth"
predicate could be replaced by the following predicates:
1. islaw(c,p), which says that p is a law in the context c.
2. necessary(c,p), which says that p is provable from the laws in c.
3. possible(c,p), which says that p is consistent with the laws in c.
If you want to define A as a synonym for B(x) in the context c, you
could do so by an assertion of the following form:
islaw(c, A = (lambda x)B(x)).
I also second Vijay Saraswat's request for an updated design document
to which we can submit change proposals (such as the one in this note).