Higher-order KIF & Conceptual Graphsfritz@rodin.wustl.edu (Fritz Lehmann)
Date: Tue, 9 Nov 93 17:34:14 CST
From: firstname.lastname@example.org (Fritz Lehmann)
Subject: Higher-order KIF & Conceptual Graphs
Cc: email@example.com, firstname.lastname@example.org, email@example.com
Dear Mike Genesereth, firstname.lastname@example.org
I have gone back to "read the manual" as you
suggested, though not all of it this time. I noticed a
mistake of mine (back in September in my first email
inquiry on this matter) when I made a reference to
'uninterpreted "holds"'. I had searched through the KIF
3.0 manual for "holds" but had failed to spot its
definition (in section 8.3, Concretion).
Yes, one can _refer_ in KIF to countable sets, and
sets of these sets, as reified objects. (This includes
relations if interpreted as sets of finite, "ordered"
sequences of objects.) It isn't clear to me how actual
quantification on (the recursive closure of) these objects
has adequately expressive semantics, though, if the
interpretation is only First-Order. As I said to Pat
Hayes, it may just be that your method does preserve those
concepts and equivalences which will occur in real
applications, in which case I'm not critcizing. Let us
know. You told me to be more explicit, so here goes.
I don't understand how, after first defining a
relation with kappa-abstraction, one can then predicate
the "mixed-order" relations between it and its own
arguments (though it may be possible). If this should be
obvious from reading the manual, I missed it. I described
the practical value of this in previous messages to the
interlingua and Conceptual Graphs lists.
Also, let's look an earlier example, Charles Peirce's
(or Leibniz's) sentence: "Given any two things, there is
some character which one posseses and the other does not."
He was unable to represent this in his Beta (First-Order)
Existential Graphs, on which Sowa's Conceptual Graphs are
based. "Character" is an old word for predicate.
(Modernly, it need not be monadic.) The point of this
statement, which is a theorem in some concept-systems, a
possible axiom in others, and false in still others, is to
give a criterion for the distinctness of two individuals.
Some database theories assume it and some don't.
John Sowa requested that I formalize that sentence.
In true second-order logic I'd say: "Ax,y (~(x = y) -> EP
((P(x) & ~P(y)) v (P(y) & ~P(x))))". The "Exists P" makes
it second-order; the disjunction may be droppable. It is
not obvious to me how to convert this correctly to First-
Order KIF or Conceptual Graphs. Perhaps you will do it
very simply. Apparently one cannot in the definition
assume that distinctness of individuals is already
My motivation for this is that I am exploring
automated knowledge base integration, which has practical
commercial value. This means starting with two knowledge
bases with very different concept-systems and taxonomies
("ontologies") and discovering automatically the
correspondences (identities, inclusions and overlaps)
between concepts (and relations) in one and those in the
other, and then using these correspondences for combining
the two into an integrated knowledge base. Another use of
the correspondences is automatic translation from one
knowledge system to the other. When the two systems
"first meet," they mutually explore the highest, genuinely
ontological, levels of their concept-systems in order to
find some common ground for communication. I think of
this as "ant feelers" when strange ants meet on a path.
I'm hoping that KIF and CGs will be suitable knowledge
languages for this. Finding out the criterion for
distinctness is an early priority, so the truth of
Peirce's sentence in an ontology comes up soon.
In KIF all predicable objects are subdivided into the
two disjoint classes of sets and individuals. (7.1). The
problem here is to determine, for a particular ontology,
when a pair of differently described objects refers to a
set-object (of two individuals) or to one individual
object (or singleton), and conversely, when a single
description must denote just one individual or may denote
Speaking slightly imprecisely for brevity: in all
systems I've seen, the more some individuals number, the
fewer the predicates (descriptions or containing sets)
they share in common; dually, the more the predicates (or
containing sets), the fewer the individuals which they all
apply to or contain. This forms an "adjointness" between
individuals/tuples and predicates, in some cases a so-
called "Galois connection". In pure First-Order systems
based on finite sets, the Galois connection between the
powerset of monadic predicates and the powerset of
individuals is a dual isomorphism (of Boolean lattices).
So, for the finite case at least, Peirce's sentence seems
to be a logically-true theorem. I would guess (by Stone's
Theorem?) that it's a theorem for the countable case.
(I'm researching the n-adic case with identiity.). In
higher-order, approximative and intensional systems, there
is still a Galois connection, but it is no longer a dual
isomorphism. Then Peirce's sentence may or may not be an
axiom (as far as I can tell). In inchoative systems (in
the sense of Parker-Rhodes' "Theory of
Indistinguishables") there is a kind of adjointness but it
does not look like a true Galois connection. Then
Peirce's sentence is false. If any of this is wrong,
someone please correct me.
I've come across about 117 existing concept-systems
and I'm still seeking and finding new ones. (The hope is
to exploit some of the person-centuries of thought and
work that have gone into existing concept-taxonomies and
specialized thesauri.) All three types described above
occur, and they potentially need to be able to
communicate. Even if Peirce's sentence is somehow
obliquely suggestible in KIF or CGs by an analogous
logically-true First-Order theorem on sets, this seems to
make it impossible to define concepts in systems in which
it is inherently contingent or false. In higher-order
logic there is no problem since the Peirce sentence is
easily expressed. Maybe you can straighten me out on this
Another important issue for me is the higher-order,
large-scale structure of concept hierarchy, in particular
the ability to factor it into separate, structured
"aspects" (a.k.a. dimensions, facets, determinables,
attributes, poset-factors, or Aristotelian categories).
My KIF 3.0 manual (June, 1992) omits the
axiomatization of numbers. At the end of October I asked:
"'All monotonic functions of 42 have positive values.'
Not very exotic, but can anyone express it correctly in
KIF?" I would still like to see your answer, which might
be trivially easy. The question is, does it really
quantify over ALL monotonic functions? No matter how
weird or recursive they are, they still have positive
values for 42.
(Incidentally, KIF's requirement that all systems
support its complicated number scheme seems a bit
burdensome for implementers. I wonder how many ontologies
will actually need to use "cis (x)" --- the complex number
"(cosin(x radians)+ isin(x radians)". Hey, if we all need
to support complex numbers, why not quaternions? Cayley
numbers too. And Sylvester numbers! What's the principle
for the cut-off?)
The concept "infinite" occurs in some form in many
ontologies. If there is a First-Order KIF definition,
what is it? (If the answer is "read the manual" please
give page numbers since there's no index in my copy.) I
believe that the usual version of "infinite" is only
higher-order definable. Barwise & Feferman's model theory
collection mentions numerous other notions definable in
higher-order but not in First-Order, like countable, well-
ordering, natural numbers, real numbers, etc., and the key
properties of theories of things like ordered Abelian
Groups, various kinds of automata, trees; topolological,
compact & Hausdorff spaces; complete partial & linear
orders, lattices, and Boolean algebras; Scott-type
domains, probabilistic systems, etc. At least some of
these have practical applications. It seems a shame to
disqualify them all from representation in a "universal"
knowledge representation language.
You asked what I recommend. As my earlier messages
have said, I tentatively favor true classical n-order,
(poly)n-adic logic semantics, or at least something which
will accomplish the same things in all practical
applications. I'm not yet persuaded that incompleteness
or uncompactness are important practical considerations
for knowledge interchange.
Yours truly, Fritz Lehmann
PS. My very parenthetical comment to Pat Hayes about
Cantor's Theorem isn't relevant to knowledege interchange,
since very few people share my skepticism.
4282 Sandburg, Irvine, CA 92715 USA 714-733-0566