# definitions and analytic truth

Robert MacGregor <macgreg@isi.edu>
Message-id: <9201031635.AA02718@quark.isi.edu>
To: interlingua@isi.edu
Subject: definitions and analytic truth
Date: Fri, 03 Jan 92 08:35:30 PST
From: Robert MacGregor <macgreg@isi.edu>

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)))
I am hoping that the proposal has progressed beyond this
stage. If not, then I will take this occasion to lodge
some specific objections.
Given the above example, are the following statements
equivalent?
(analytic-truth '(<=> (A ?x) (B ?x)))
and
(analytic-truth '(<=> (B ?x) (A ?x)))
If they are, then presumably the following two statements
are also equivalent (but shouldn't be):
(defrelation A ?x (B ?x))
and
(defrelation B ?x (A ?x))
If they are not, then we observe that the iff operator
"<=>", which is normally considered to be commutative,
does not necessarily commute when used inside of a quote.
I would consider this bad language design -- an operator
ought to have a uniform usage throughout a language.
Also, is the following statement legal:
(analytic-truth '(<=> (and (A ?x) (B ?x))
(and (C ?x) (D ?x))))
If not, how does KIF stipulate what is a legal analytic
truth and what isn't?
Personally, I find the notion of analytic truth to be
valuable, but object both to the use of the iff operator
as a characterization of a definition, and I object to the
use of the quotation device as a means for defining
"defrelation".
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?
Cheers, Bob