definitions and analytic truth

schubert@cs.rochester.edu
Date: Tue, 7 Jan 92 19:00:05 EST
From: schubert@cs.rochester.edu
Message-id: <9201080000.AA06640@ash.cs.rochester.edu>
To: interlingua@isi.edu, sowa@watson.ibm.com
Subject: definitions and analytic truth


JMc's proposal to take the domain assertion for

  (defobject <name> <wff1>...<wffn>)
to be
  (=> (exists <name> (and <wff1>...<wffn>)) (and <wff1>...<wffn>))

seems to solve the problem of inconsistent definitions he raised. One 
slight syntactic glitch is that in KIF names (constants) are distinct 
>From quantificational variables. JS's proposal to use the Hilbert epsilon
operator would be one rather nice way around that. However, if we want 
to stick to more familiar constructs, we could write the domain assertion
as

  (=> (exists <var> (and <wff1'>...<wffn'>)) (and <wff1>...<wffn>))

where <var> is a variable not occurring in wff1,...,wffn, and wffi'
is the result of substituting that variable for all occurrences of
<name> in wffi.

Another way would be to change the syntax of defobject to explicitly
use predicates, rather than sentences, as constraints on <name>, i.e.,

  (defobject <name> <pred1>...<predn>)

where the <predi> are monadic predicates (possibly lambda-abstracts).
Then the domain assertion could be stated without substitution as

  (=> (exists ?x (and (<pred1> x)...(<predn> x)))
            (and (<pred1> <name>)...(<predn> <name>)))

Another possibility, as RF notes, is to use 

  (defobject <name> <term>),

but as he points out, we would then have no way of defining an object
by specifying a set of (definitional) axioms about it. The earlier
options are less restrictive. (_Substitutional_ definitions, as
they've been tentatively formulated by me, do essentially impose this
restriction.)

(By the way, note that KIF doesn't currently have a way of defining
_functions_ by specifying a set of (definitional) axioms about them.
If it did, we would again encounter JMc's problem, and its resolution 
would apparently require second-order existential quantification.)

There are other possibilities, such as appeal to Frege's "nonexisting
object" (which has been put to good use in semantics of definite
descriptions, e.g., in Aldo Bressan's "general interpreted modal 
calculus"), but I favor the option based on variable substitution as 
the least esoteric.

I'm wondering if JMc and DAM think that with the fix JMc proposes, the
definition facility as outlined by RF now conforms with their precepts 
-- or do the constructs still allow us to "sneak in new assertions"? 
In particular, if we use defprimrelation to define a type hierachy 
(which the syntax certainly permits) are we "sneaking in new assertions"?
(This issue is quite independent of whether we OUGHT to use 
defprimrelation that way. I would rather not, though I don't feel 
as strongly about it as JS seems to. My impression is that in much of 
the KR community, "terminological knowledge" is taken to cover roughly 
the sorts of information one finds in dictionary definitions, including 
type subsumption. As long as we make a clear distinction between which
definitional constructs conform with the mathematical logician's
notion, and which ones are more like the lexicographer's, this should
not cause problems.)

A question about lambdas versus universals in domain assertions (i.e.,
the alternatives noted by RF): I'm not convinced the two versions are
distinct, even with sequence variables. Doesn't the lambda-version
(or kappa-version) allow vacuous abstraction (abstraction of variables
not occurring in the body) just as the universal version allows
vacuous quantification? And isn't something like

   P = (kappa ($x $y) (Q $x))

equivalent to

   (forall ($x $y) ((P $x $y) <=> (Q $x)))?

Finally, the question of whether definitions should count as sentences
and have truth values seems to hinge on the status of sentences
containing quotation. RMc suggests that the content of a definition
consists of the domain assertion along with an assertion like 
(define '<name> '<defining-expressions>). Yet he opposes sentential
status for definitions. But isn't the latter a sentence? If not,
what is it? We might say, it's a sentence of the metalanguage, but not
of the object language. However, though the KIF document does talk
this way (in some places), there's every indication (including in the
formulation of a revision-semantics for truth, and in the suggested
approach to modals) that quotation is earmarked for use in the _object_
language -- i.e., a knowledge base may properly contain assertions
with quoted expressions, and the theory of truth and entailment will
cover these).

-Len Schubert