Definitions and analytic truth

• Mail folder: Interlingua Mail
• Next message: David McAllester: "KIF"
• Previous message: John McCarthy: "Definitions and analytic truth"
• In-reply-to: John McCarthy: "Definitions and analytic truth"
• Reply: schubert@cs.rochester.edu: "definitions and analytic truth"

Message-id: <199201071204.AA06686@venera.isi.edu>
Date: Tue, 7 Jan 92 07:03:11 EST
From: sowa@watson.ibm.com
To: fikes@sumex-aim.stanford.edu, jmc@cs.stanford.edu
Cc: interlingua@isi.edu, cg@cs.umn.edu
Subject: Definitions and analytic truth

Yes, I agree with John McCarthy's point:

> I think you are correct that only defobject gives problems, but it
> does give problems if you leave it as is.  In it's most brutal
> form it allows
>
> (defobject foo (= foo 0) (= foo 1))

Defining types and relations that have no instances does not create
a problem, but defining an individual that does not exist is awkward.

John's proposed solution is very close to Hilbert's epsilon operator:

> The most straightforward way of getting around this is to let
> (defobject <name> <sentence>) generate the sentence
>
> (implies (exists <name> <sentence>)  <sentence>),
>
> i.e. the existence of an object satisfying <sentence> implies
> that <name> satisfies <sentence>.

Hilbert defined the term

     (epsilon x)P(x)

as selecting an arbitrary x for which P(x) is true.  If there is only
one solution, it gives you the same individual as Russell's iota
operator.  But if there is no solution, Hilbert defined it as giving
you an arbitrary element of the domain (but there is no way of knowing
which element it is).

Given the epsilon operator, you can define the quantifiers:

     (Ex)P(x)  is defined as  P((epsilon x)P(x)).

     (Ax)P(x)  is defined as  P((epsilon x)(not P(x))).

There is a nice little book that starts with the epsilon operator
and builds up all of first-order logic in terms of it:

   Leisenring, A. C. (1969) _Mathematical Logic and
   Hilbert's epsilon-Symbol_, Gordon and Breach, New York.

Leisenring shows that epsilon operators give you some powerful
proof techniques that can simplify certain kinds of problems.

In conceptual graphs, the simplest graph is a single concept,
such as [CAT].  The formula operator phi, which translates CGs
into predicate calculus, gives you the following:

    phi([CAT])  =  '(Ex)cat(x)'

And the referent of the concept [CAT] is defined as an epsilon term
(epsilon x)cat(x).  That is consistent with the requirement that
the predicate that defines the type of a concept must be true of
the referent of that concept:  cat((epsilon x)cat(x)).  By Hilbert's
construction, this property is even true for the concept [UNICORN].
This is just one example of the way the epsilon operators give
a satisfying sense of completeness to the theory.

In an earlier note, I said that I would like to see just one basic
definitional operator that associates a name with an expression.
If you introduce epsilon terms into the language, defobject would
be equivalent to

     (define <name> <epsilon-term>).

This definition has the property that McCarthy suggested above.

John Sowa