Date: Sat, 28 Jul 90 06:49:26 -0400
Message-id: <>
Subject: definitions-proposal



Judging from the amount of discussion that has gone on, the syntax 
and semantics of definitions is considered a very important issue.
The following tentative proposal was produced in response to some
prodding from Rich, who thought that Ron's remarks about 
substitutional definitions and my further comments should be
developed into a technical proposal for the interlingua. The
result is rather more lengthy, involved and incomplete than I 
had hoped...


I think part of the problem in the ongoing discussion of definitions
has been the fact that we haven't gotten clear about whether 
definitions are object language or metalinguistic constructs. My
view is that we can sensibly, and usefully, have both. So I'll first
propose a metalinguistic syntax for substitutional definitions, and
then comment on the meaning of object-language definitions. (I'll
refer to the latter as "analytic definitions", for reasons to be

The metasyntax for substitutional definitions is not to be confused
with Mike's syntax of "metalevel knowledge", based on quotation.
The latter, insofar as it is aimed at expressing notions like 
necessity and belief, is part of the interlingua proper - the 
language used to describe the domain of discourse (which by fiat
includes the entities describable using quotation, viz., expressions).
The metalinguistic constructs below are in "meta-interlingua" (meta-
KIF?); they say NOTHING about the domain. I will later speculate,
however, whether this metalinguistic knowledge can be pulled down
to the object level using the (very rich) resources of KIF.


A substitutional definition provides some new (often more concise)
way of writing some class of object-language expressions. The paradigm
examples are definitions of new symbols in logic texts, such as

   phi <=> psi  =def  (phi=>psi)&(psi=>phi)


  (E alpha)phi  =def  ~(alpha)~phi

where phi and psi are wffs and alpha is a variable. These definitions
sanction free use of the defined symbolism in the object language,
and the meanings of the new symbols are not independently defined.
Rather, the constructs in which they participate have whatever meaning
results upon substitution of the defining expressions for the defined
expressions. There is an obvious analogy to macros, EXCEPT that the
defined expressions need not in general be replaced by defining
expressions before inference begins; rules of inference can be DERIVED
>From those originally given, covering the new syntax. In other words,
substitutional definitions can provide genuine EXTENSIONS of the 
object language.

The problem, then, is to provide a formalized metasyntax for the above 
kinds of informal definitions. One thing that's immediately clear,
if we want to match the flexibility of the logicians' definitions, 
is that in general we need to be able to specify not just substitutions
for individual defined symbols, but for PATTERNS OF USE of defined
symbols (like the use of "<=>" flanked by formulas). Sometimes, we
may want to use the same defined symbol in different patterns (see ":"
in examples 3 and 4 below). Occasionally, we may even want to specify 
patterns of use involving multiple defined symbols ("E" and ":" in
example 5), or multiple occurrences of the same defined symbol (example

To specify patterns of use, we need METAVARIABLES (schema variables) 
to stand for various kinds of expressions of the object language - 
variables, sentences, terms, and so on. We need a distinguishable 
type of atom for these, and I will use prefix $$ for individual 
metavariables and prefix @@ for sequence metavariables. (A couple 
of other possibilities:

   object-level variables           metalevel variables
    individual  sequence           individual  sequence

         ?x       $x                  ??x       $$x
         ?x      ??x                   $x       $$x       

As header of these definitions, I suggest METADEF, to ensure a clear
distinction from object-level definitions like defrelation and

With these preliminaries, a substitutional definition may be
formalized as an expression of form

    (METADEF sigma1 sigma2)

  (1) sigma1 is an (object-level) atom or a list of (object-level)
      atoms and metavariables (with repetition allowed);
  (2) the sigma1-pattern must not be unifiable with the sigma1-
      pattern of any other METADEF (where only metavariables
      function as unification variables); this prevents ambiguity;
  (3) sigma2 is an (object-level) atom or list structure, whose
      ultimate atomic constituents are (a) object-level atoms, but
      excluding at least one of the atoms of sigma1; the excluded atoms
      are called the DEFINED symbols; (b) metavariables, including all 
      those and only those appearing in sigma1; and possibly, (c) 
      metalevel function symbols, which can appear only as heads of 
      list structures; (metafunctions are distinguished by prefix "#"
      and must have algorithmic definitions);
  (4) sigma2 must contain no unbound object-level variables (but it
      may contain quantified variables); this prevents "accidental
      binding" by external quantifiers; and
  (5) any defined symbol of the METADEF that appears in another 
      METADEF must be a defined symbol there as well.

The intended notion of "object-level atom" includes new logical atoms
(such as new quantifiers and logical connectives) and defined
"punctuation" signs (see examples) as well as the atoms listed in 
table I of the KIF document.

EXAMPLE 1: renaming an atomic symbol

 (METADEF & and)                      Note: the defined atom is "&"

EXAMPLE 2: changing the logical syntax

 (METADEF (@@x ==> $$y) (=>@@x $$y))  Note: the defined atom is "==>"

EXAMPLE 3: introducing a new "exists" syntax

 (METADEF (exists $$x : $$y $$z) 
          (exists $$x (and $$y $$z))) Note: the defined atom is ":" 

EXAMPLE 4: introducing a new "forall" syntax

 (METADEF (forall $$x : $$y $$z)
          (forall $$x (=> $$y $$z)))  Note: the defined atom is ":".
                                      Examples 3 and 4 are compatible,
                                      since the patterns do not unify.
EXAMPLE 5: variant of example 3

 (METADEF (E $$x : $$y $$z)
          (exists $$x (and $$y $$z))) Note: the defined atoms are "E",":"

EXAMPLE 6: introducing a new quantifier ("there is exactly one")

 (METADEF (E! $$x $$y)
          (exists $$x (and $$y 
                           (forall (#UNUSEDVAR $$y)
                                   (=> (#SUBST (#UNUSEDVAR $$y) $$x $$y)
                                       (= (#UNUSEDVAR $$y) $$x) )))))

  where #UNUSEDVAR is a 1-place metafunction whose value is the first
  (object-level) individual variable not appearing in the given argument
  expression, in some fixed enumeration of infinitely many (object-level)
  individual variables; and #SUBST is a 3-place metafunction whose
  value is the expression obtained by substituting the expression
  given as first argument for all free occurrences of the atom given 
  as second argument in the formula given as third argument.

EXAMPLE 7: abbreviating a compound formula, using "bachelor"

 (METADEF (bachelor $$x) (and (male $$x) (not (married $$x))))

                                     Note: the defined atom is "bachelor"

EXAMPLE 8: abbreviating another compound formula, using "isa"

 (METADEF ($$P isa $$Q) (nec-a '(forall $x (=> ($$P $x) ($$Q $x)))))

                                     Note: the defined atom is "isa";
                                           "nec-a" is discussed below

EXAMPLE 9: "abbreviating" a functional expression

 (METADEF (paternal-grandfather $$x) (father (father $$x)))     

                      Note: the defined atom is "paternal-grandfather"

EXAMPLE 10: changing the syntax of enumerated sets

 (METADEF (: @@x :) (set-of @@x)) 

          Note: the defined atom is ":"; "set-of" is assumed to be
                a set-forming object-level function


Why at All?

The first question one might ask is, why provide for metalinguistic
substitution at all? In a general KR, one would want such a facility
for convenience, conciseness and perspicuity of expression. But why
allow it in an interlingua? One good reason, I think, is to make it
easier to build translators from other KR's to the interlingua.
Much of the work of building a translator then comes down to writing
METADEFs, rather than programming. (A routine for replacing defined
constructs will presumably already exist.)

Of course, to the extent that substitutional definitions extend the
interlingua itself, the defined constructs in principle need not be
replaced at all - except for a couple of problems: OPERATIONS defined
on the interlingua, such as storage, retrieval, or perhaps inference
probably will be defined only for the "basic" syntax, not for extensions
via substitutional definitions; and translation from one external KR
to another via the interlingua will surely require reduction to the
"basic" syntax.

Quotation Meets Substitution

An important technical question that is raised by the availability of
quotation in the object-level syntax is whether substitution of
defining constructs for defined constructs is permissible within the
scope of quotation. Suppose, for instance, that we have indeed
introduced "&" as a synonym for "and" as per example 1. Can we then 
       (bel john '(and (pretty mary) (intelligent mary)))
       (bel john '(& (pretty mary) (intelligent mary))),

and vice versa? One is inclined to say "yes" unhesitatingly. But now

       (contains-a-3-char-atom '(and (pretty mary) (intelligent mary))).

With "contains-a-3-char-atom" interpreted as you might expect, this is
clearly a true statement. But if we now write

       (contains-a-3-char-atom '(& (pretty mary) (intelligent mary))),

we seem to have a false statement. After all, "&" IS a lisp atom, and
quoted expressions are interpreted as denoting those expressions, in
the lisp sense. So we seem to be in a quandary.

One way out would be to make a syntactic distinction between basic
and defined atoms. For instance, defined atoms might all start with
"&". The understanding would be that defined constructs (containing
&-atoms) are not only meaning-equivalent, but even list-structure
equivalent to their definitions. They "appear" to have a certain
structural constitution, but their "actual" structural constitution
is as specified in the appropriate definition. An unattractive aspect
of this solution is that list structures under quotes will no longer 
be what they seem; and the notation including defined symbols will 
be slightly less concise and readable than one might have hoped 
(e.g., in the use of ":" as punctuation).  Another possibility would 
be to limit the use of defined symbols to unquoted contexts. However, 
this has the even greater disadvantage of preventing use of convenient 
defined symbolisms in statements expressing belief, necessity, etc.

I am strongly inclined toward the first alternative: we just have to
accept that quotation is transparent to substitutional definitions;
(is-a-3-char-atom '&) is true if "&" has been defined as shorthand
for "and". I have not introduced distinctive atoms for defined
symbols because I am not sure what distinctive notation to use, and
because the distinction could in principle be kept implicit. (It is
certainly easily determinable from the METADEFs which symbols are


The proposed syntax involves some rather difficult choices concerning
expressiveness. The following are some of the issues.

1. One might forego the generality of logicians' definitions, and
   insist that sigma1 (the "pattern of use" of the defined atom(s)) 
   always be an atom, namely the one being defined. This would allow 
   only example 1 above, and abbreviations of ground terms and
   closed formulas. However, if the basic interlingua were expanded
   to allow lambda abstraction, then predicate and function definitions
   with much the same effect as the abbreviatory definitions in 
   examples 7 and 9 could be specified. For example, we might write

   (METADEF bachelor (lambda $x (and (male $x) (not (married $x))))),

   which would give the same abbreviations as example 7, after
   lambda-conversion. In this more restrictive substitutional syntax,
   there would be no need for metavariables and metafunctions. On the
   other hand, examples like the definition of "there exists exactly
   one" (ex. 6) and "isa" (ex. 8) could not be handled (the latter 
   because it would require abstraction of PREDICATE variables, which 
   we would probably not want to allow).

2. One might insist that metafunctions be drawn from a fixed,
   predetermined set (including #UNUSEDVAR and #SUBST). The hazards
   of not imposing any restrictions are obvious (e.g., lack of
   assurance of efficiency, correctness and termination; inability
   to do "compile-time" syntax checking on definitions). However,
   its unclear to me what a minimally adequate set should contain.

3. One might want to provide for type constraints on metavariables
   as a means of facilitating syntax checking. The METADEF syntax
   might then be
     (METADEF sigma1 sigma2 pi1 ... pik)

   where each constraint pij is of form (<metapredicate> <metavariable>),
   the metapredicates essentially being those appearing in angle
   brackets in tables I-III in the KIF document (e.g., #INDVAR,
   #RELCONST, #ATOM, #FUNTERM, #SENTENCE,...) and the metavariables
   being those which appear in sigma1 and sigma2.

   This would make it possible to check whether a given definition
   will give a legal interlingua expression upon replacement of 
   expressions matching the defined form sigma1 (especially if
   the metafunction repertoire is tightly constrained, or at least
   their output types are specified).  It would also allow more
   "fine-grained" distinctions in the patterns of use: patterns
   would not be considered unifiable if unification would violate
   the type constraints of the metavariables. 

   I find this refinement quite attractive. However, I wouldn't 
   favor making constraints obligatory, as that would be a nuisance 
   for most simple definitions.

4. A question arises whether symbols (and the corresponding constructs)
   defined in other METADEFs might be allowable in the replacement   
   pattern, sigma2. This would appear to be harmless if there is no
   cyclic reference to defined symbols (e.g., METADEF1 defines S1
   but with introduction of defined symbol S2; METADEF2 defines S2
   but with introduction of defined symbol S1). Checking for cycles 
   is not hard. Thus condition (5) could be weakened.

Other issues 
- Constructs defined via METADEF are eliminable, as they should be
  (cf., David McAllester's comments)

- David's problem concerning recursive definitions certainly remains,
  though as far as I can see that is a problem concerning the
  expressiveness of the object-level language which arises independently
  of the choice of substitutional metalanguage. Isn't this the same
  problem as that of proving universally quantified statements of
  arithmetic? If the interlingua allowed axiom SCHEMAS, in particular
  an induction axiom schema, we could axiomatize "descendant" as
  "level-n descendant, for some n", and prove that all descendants
  of a human are human. The alternative of using a minimization
  operator to obtain fixed points of recursively defined functions
  sounds interesting, and worth exploring. 

  But I think there are independent reasons for wanting a syntax for 
  axiom schemas, such as that we often want to give axioms for a whole 
  class of predicates, or a whole class of sentential forms (such as 
  the logical axioms of axiomatic logics). Now it may well be (though
  I haven't given it much thought) that all the axiom schemas we
  want are already expressible in KIF. For instance, we might express
  "The first argument of all mental-action predicates is human" as

    (forall $p (=> (mental-action-pred-const $p)
                   (true '(=> (,$p $x @y) (human $x)))))

  Despite appearances, this isn't second-order logic, since $p is
  a variable over syntactic objects (predicate constants), not over
  predicate denotations. (However, I think the semantics of "true"
  as given in the July KIF document is in need of amendment.)
  Similarly, it seems that even induction can be formalized in this
  sort of way, roughly along the lines

    For all p, if p is a sentence with one free variable x, then
    if subst(0,x,p) is true and [for all x, if p then subst(succ(x),
    x,p)] is true, then for all (integers) x, p is true.

  So that would allow solution of the "descendant" problem, though
  probably not as neatly as one would like. By the way, it's worth
  noting here that the KIF document uses equality and arithmetic
  functions, it does not assign them any special semantics at this
  point, leaving them rather as freely interpretable relations or

- One may wonder whether the quotation mechanism also allows one
  to "pull down" metalinguistic definitions into the object language.
  (I imagine that was Mike's intention with the original "defines"
  notation, which involved quotation.) One might expect this to be
  possible in principle, since KIF can describe list structures and 
  talk about their meaning. The question is whether the informally 
  understood meaning of METADEFs - that they LICENCE certain classes 
  of substitutions, with preservation of meaning - can be declaratively

  Let's give it a try for a few of the earlier examples. I'll use
  a predicate "substitutable" over expressions which I'll later try to
  express in terms of other notions.

  EX.1: (substitutable '& 'and)

        (Note: as long as we only substitute for atoms, without regard 
        for pattern of use, it doesn't really get any harder than that!)
  EX.2: (forall $x (=> (sentence $x)
                       (forall $y (=> (sentence $y)
                                      (substitutable '(,$x ==> ,$y)
                                                     '(=> ,$x ,$y) ))))
  EX.6: (forall $x (=> (indvar $x)
                       (forall $y (=> (sentence $y)
         (substitutable '(E! ,$x ,$y)
          '(exists ,$x (and ,$y (forall ,(unusedvar $y)
                                        (=> ,(subst (unusedvar $y) $x $y)
                                            (= ,(unusedvar $y) ,$x))
  Similar axioms can be provided for the remaining examples. The axioms
  are not easy to write, because of the worry about getting the quotes 
  and commas right. In the last example, "unusedvar" and "subst" are
  ordinary expression-denoting functions over expressions. However,
  it is clear that the axioms will be useless for actually "inferring
  explicit substitutions" unless there is a means of inferring standard
  names for the values of the functions -- e.g., by computing them.

  Now what does "substitutable" mean? Part of it (perhaps all of it) is
  that substitution of one for the other preserves meaning:

    (forall $x 
      (forall $y (=> (substitutable $x $y)
                     (forall $z (synonymous (subst1 $x $y $z) $z)) ))),
  where subst1 is the result of substituting $x for the first occurrence
  of $y in $z. In turn "synonymous" implies equality of denotation:

    (forall $x
      (forall $y (=> (synonymous $x $y)
                     (= (denotation $x) (denotation $y)) )))

  However, the converse doesn't hold. For instance, denotationally 
  equal expressions are not in general interchangable in modal contexts,
  and in that sense non-synonymous. At least, that is so if "denotation"
  is identified with "extension" (semantic value defined extensionally
  as for KIF). I leave the problem there. Clearly it is not a simple
  matter to represent metalinguistic substitutional definitions in the
  object language, and it appears more practical at this point to make
  direct use of a metalinguistic syntax.


I use the qualifier "analytic", since it seems to me that the kinds
of definitions offered in the KIF document using defrelation,
defprimrelation, and so on, are the basis for what have traditionally
been called "analytic truths", such as that every bachelor is unmarried,
or that if x kills y, then y dies.

Part of what is needed to understand the semantics of definitions, I
suggest, is the recognition that they do not only assert a factual
sentence about a domain (e.g., that bachelors are unmarried males), 
but also that this sentence IS definitional (i.e., that the SENTENCE 
to the effect that bachelors are unmarried males IS a definitional 
sentence). I will call the first part the "domain assertion" implicit
in a definition and the second part the "syntactic assertion".

Something else needed to do definitions semantic justice, I believe, 
is some appropriate notion of necessity. Analytic truths are NECESSARY 
truths, in virtue of the meanings of the words (predicates, etc.) used.
Let's call this notion of necessity "nec-a".

It's clear that this notion of necessity is dependent on the set of 
definitions as a whole. One way of giving expression to this intuition
is to say that (nec-a phi) holds just in case it is a logical
consequence of the domain assertions implicit in the definitions; 
i.e., if DEFS(delta) picks out the domain content of analytic 
definitions in knowledge base delta, then
      t  ((nec-a phi)) = true iff DEFS(delta) |= phi
(This is not unproblematic, since it makes truth dependent on entailment,
which is itself dependent on truth. But I will make no attempt to work
out details.) Note that even though DEFS(delta) ignores the syntactic
assertional content of definitions, it is well-defined only to the 
extent that definitions are effectively recognizable as such -- and 
THAT is what the syntactic assertional content is needed for. 

There is also an assumption here that the set of definitions in the 
knowledge base is complete, in the sense that there are no "missing 
definitions" which, if only we knew them (or had gotten around to 
stipulating them) would allow us to prove additional analytic truths. 
(If the last condition is not met, nec-a will be nonmonotonic. However,
only negative assertions ~(nec-a phi) may have to be revoked, not 
positive ones.) Given this completeness assumption, we also know
that the sentences of the knowledge base NOT asserted to be definitions

If the currently proposed KIF syntax for analytic definitions 
("defrelation", etc.) is adopted, it will be important not to treat 
this syntax as part of the ordinary object language. Rather, such
definitions should be viewed as simultaneously asserting a domain
sentence (whose ordinary object-language form has to be "assembled"
>From several pieces), and the fact that this domain sentence IS 
definitional (i.e., part of DEFS(delta)).

A more explicit way of doing the same thing, using only the ordinary
object language (but exploiting quotation), would be to say something 
like (definition '(...)) or (meaning-postulate '(...)); e.g.,

   (definition '(forall $x (<=> (bachelor $x) 
                                (and (male $x) (not (married $x)))))).

The contribution to DEFS(delta) is then given explicitly by the 
quoted argument (without the quote). And in addition, the definition
as a whole makes the needed syntactic assertion about the status of 
the domain sentence.

If one wanted to be explicit about what the definition is a definition 
OF, one could use the even more explicit syntax (at the risk of 
confusion with the other options under consideration)

   (defrelation 'bachelor '(forall $x (<=> etc. )))

But at least for the purpose of deducing analytic truths, the 'bachelor
argument is not needed.

I favor the explicit syntax (the second-last or last), because it
involves no extension of the basic syntax or semantics. The semantics
of nec-a, along the lines suggested, is a novelty, but I think
something of this sort is unavoidable no matter what syntax is
chosen for definitions. (Well, maybe nec-a could be encoded as
provability from formulas phi for which (defintion 'phi) is known
to hold. Provability in principle requires no new semantic notions.)

The same syntax, or a slightly different syntax can be used for
primitive relations, except for use of one-way implication. The
treatment of functions is similar, except that it involves universally
quantified equalities, rather than equivalences or implications.
Similarly for object definitions.

So, what is provable from definitions? Well, for one thing, since
the domain sentence phi contributed to DEFS(delta) by a definition
is certainly provable from DEFS(delta), it follows that the sentence
(nec-a phi) is provable as well (in view of the semantic definition
of nec-a). Therein, I think, lies the intensional content of 
definitions.  As well, it will be provable that this sentence
IS a definition, especially if this has been explicitly asserted as
above. Note that it won't be possible to prove that a sentence is
a definition if it wasn't put in as a definition, since there are 
(presumably) no axioms which allow the conclusion that something
is a definition from general premises. It will also be possible to
prove such things as that John does NOT believe there is a married
bachelor, if it is known that John believes no analytic falsehoods:

  (forall $x (=> (sentence $x) 
                 (=> (nec-a '(not ,$x)) (not (believes john $x)))))

This seems to me like the right sort of inferential behavior.
None of this is very precise or well-worked out (time is short), but 
I hope it provides some clarification, or directions in which to seek 
clarification. The upshot for me is that virtually any of the 
suggestions concerning defrelation, defprimrelation, etc., that 
have been made in the definitional debate could be made formal sense 
of, although some of the suggestions will keep the interlingua "purer" 
and more uniform than others.