definitions and analytic truth

• Mail folder: Interlingua Mail
• Next message: Vijay Saraswat: "Re: definitions and analytic truth "
• Previous message: sowa@watson.ibm.com: "Supporting SQL, EXPRESS, etc., with a logic-based standard"
• Reply: Vijay Saraswat: "Re: definitions and analytic truth "

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