definitions and analytic truth

schubert@cs.rochester.edu
Date: Fri, 3 Jan 92 18:45:04 EST
From: schubert@cs.rochester.edu
Message-id: <9201032345.AA02348@ash.cs.rochester.edu>
To: interlingua@isi.edu, saraswat@parc.xerox.com, sowa@watson.ibm.com
Subject: definitions and analytic truth

John and Bob,

Concerning the proposed semantics of definitions in the interlingua,
John comments

>I like that approach.  But there should also be additional "laws" or
>"axioms" besides the definitions.  In geometry, for example, points
>and lines are never defined, but their possible interactions are
>determined by a set of axioms.

This is the point I was getting at in my message when I said definitions
may only partially constrain the terms defined.

Specifically, the definitional constructs under consideration in the
interlingua are

  (defobject <name> <wff1> ... <wffn>)
  (defunction <name> (<var1> ... <varn>) <wff>)
  (defrelation <name> (<var1> ... <varn>) <wff1> ... <wffm>)
  (defprimrelation <name> (<var1> ... <varn>) <wff1> ... <wffm>)

(We might also use a single "definition" construct which subsumes all
of these, essentially quoting their parts; there are pros and cons to
this...) The first 3 presume "full" definitions (and only one definition
may be given per name), but the last allows partial "definitions", and
there may be any number per name, each one placing some constraint on
the "defined" term. The example in the draft document handed out at
one of the working group meetings was

  (defprimrelation person ($x)
     (mammal $x))

In this way we can write down any number of "laws" about how terms are
related, without fully defining them.

I think a reasonable complaint here is that such laws aren't, and
shouldn't be called, "definitions"; in fact, note that it can be rather
arbitrary what name we insert at the head of defprimrelation. For
instance, if we want to say, as a "law", that no whale is a fish
(i.e., no fish is a whale!), is this a partial definition of "whale"
or of "fish"? Still, the consensus in the interlingua group seemed
to be that the use of partial definitions, with the partial definition
attached to a particular name, was so entrenched in KR languages that
it made sense to have such a construct in the interlingua. I should
also point out that the "analytic-truth" predicate (below) in principle
affords a means to express laws WITHOUT attaching them to particular
names.

Bob comments,

>I'm curious to know the status of definitions in KIF.
>The last thing I saw was that a definition of a
>form similar to
>   (defrelation A (?x) (B ?x))
>(I may not be using exact KIF syntax, but I think you get
>the idea) was called equivalent to 
>   (analytic-truth '(<=> (A ?x) (B ?x)))

(Aside: Bob prefers ?x where KIF uses $x; so do I.)

No, we (Rich and I) decidedly didn't affirm equivalence between 
definitions and analytic truths. Rather, we proposed such analytic
truths as PART of the content of definitions (the "domain assertion"
part, in our terminology); an entailment, if you like (this depends on
viewing definitions as wffs, i.e., assertions, a view  which remains 
somewhat controversial). The notion of analytic truth was introduced 
to account for the intuitive distinction between contingent truth and
truth-in-virtue-of-meaning, the latter having necessity-like force. 

But the domain assertion of a definition doesn't capture its full
content, any more than "mammal" captures the full content of "person".
Its particular SYNTACTIC form is a crucial part of its content.
Consequently, one cannot deduce a definition from its domain assertion.
Assuming that it makes sense to talk about the truth values of
definitions (and I lean in that direction: they are true by fiat, or
convention), the draft document proposed the following truth condition 
for definitional truth (I will reformulate very slightly from the 
handout):

  (defobject <name> <wff1> ... <wffn>) 
  is true under interpretation i, variable assignment v, and definition
  set D iff 
           (normal-form (defobject <name> <wff1> ... <wffn>)) =
             (normal-form (defobject <name> <wff1'> ... <wffn'>))
  for some definition (defobject <name> <wff1'> ... <wffn'>) in D.
  Otherwise it is false.

Similarly for the other definitional forms. In other words, a definition
is true iff once it's normalized, it is syntactically identical with
the normal form of some definition in the set of definitions. The
idea is to allow small syntactic variations in a definition -- renaming
of variables, re-ordering of arguments of commutative operators, etc. --
without thereby getting a different definition. So the "normal-form"
function should standardize variables, lexicographically order
commutative arguments, etc. (Details should probably be up to users.)

So the bad consequences that (as Bob points out) would follow from
equating definitions with the (strongest) analytic truths they entail
are avoided. To come back to John's point, one could express "laws"
without committing to a particular name they partially define by
using, e.g.,
   (analytic-truth '(forall $x (=> (whale $x) (not (fish $x))))). 

Bob also says

>The traditional means for assigning a semantics for definitions
>is to make reference to lambda expressions, e.g.,
>   (defrelation A ?x (B ?x)
>is equated with something like
>   (define A (lambda (?x) (B ?x)))
>meaning that "A" is a constant that denotes a particular
>lambda expression. Rather than inventing a new and controversial
>denotation for definitions, why aren't we using something thats
>already tried and true?

I'm as big a fan of lambda as Bob (that's why I put it in my semantic
net syntax in AIJ'76 and in Hwang's & my KR for natural language in
KR'89). However, the suggestion that "(define A (lambda (?x) (B ?x))) 
just means that "A" is a constant that denotes a particular lambda 
expression" is problematic. Is the idea that "A" is just a name for 
the syntactic expression "(lambda (?x) (B ?x))"? In that case, we
are talking about SUBSTITUTIONAL rather than ANALYTIC definitions,
which were also included in the interlingua proposal as a macro-like
facility. I think one can indeed get by with substitutional definitions
wherever one might otherwise use defobject, defunction, or defrelation.
However, you can't reconstruct defprimrelation that way (and a lot of
people seem to want that notion); and since substitutional definitions 
are metalinguistic statements, you can't express them and reason with 
them IN the object language, if that's what you want to do. For instance,
you can't express that IF the definition of a bachelor is an unmarried
man, THEN Joe is a bachelor. Nor can you express the argument that since
Joe is a man but not a bachelor, it follows that the definition of a 
bachelor cannot simply be that he is a man. Nor can you express that 
Joe thinks that (the definition of) a conifer is a generally cone-shaped
tree, whereas in fact it is a cone-bearing tree or shrub. Etc.

On the other hand, if we take the above suggestion to be that "A"
and "(lambda (?x) (B ?x))" DENOTE the same thing, then this is just

  A = (lambda (?x) (B ?x)),

an object-language assertion (assuming we admit lambda into the object
language). But this leads exactly to the same problems that Bob points 
out for an interpretation of definitions as "analytic-truth" assertions.
E.g. (under standard semantics for lambda and equality), we can deduce

  B = (lambda (?x) (A ?x))

and hence (incorrectly) that (define B (lambda (?x) (A ?x))).
In fact the equalities are equivalent to

  (forall ?x ((A ?x) <=> (B ?x))).

So we would STILL want to say that (define A (lambda (?x) (B ?x)))
merely entails A = (lambda (?x) (B ?x)), but that in addition, the
fact that it IS a definition, and its particular syntactic form, are
significant. (Again I would use a normal-form function to reason 
about the truth of definitions.)
   
Finally, concerning John's further comments:

>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)).

Yes, there is a "missing argument" in the notion of analytic truth,
in the sense that there is tacit reference to a set of definitions.
This is clear from the truth conditions for definitions sketched above,
which DO refer to a particular set of definitions. I think the
suggestion to make this argument syntactically explicit is an
interesting one, requiring further thought (from my perspective,
anyway). The issue seems completely analogous to the issue of whether
modal notions like "provable", "consistent to assume", "probable", 
"known", etc. -- modalities often introduced into logics (e.g., 
nonmonotonic, probabilistic, or autoepistemic ones) -- should have
explicit "knowledge base" or "context" arguments. (In many proposals,
they don't.) 

As for the term "analytic truth" itself, it does not seem terribly
out of joint with Quine's notion. I'm not perticularly attached to the 
term, but I doubt that "necessary" is an uncontroversial substitute. 
That term, too, is loaded (since there are many forms of necessity --
logical, physical, epistemic, deontic, etc.) Moreover, I take it that
"necessary truths" are generally taken as a proper subclass of analytic
truths (see Word and Object, p.66), and I've been told (perhaps 
incorrectly) that the term "analytic truth" was used by people like
Bar-Hillel precisely to avoid confusion between truth-in-virtue-of-
meaning with (the narrower notion of) truth as a matter of logical 
necessity. But I don't think anyone views the terminological issues
as settled at this point. Maybe Quine's "truth by convention" would
serve better? Just a thought.

Len Schubert