International STANDARD FOR LOGIC: CSMF/CG/KIF
fritz@rodin.wustl.edu (Fritz Lehmann)
Date: Wed, 7 Sep 94 22:59:28 CDT
From: fritz@rodin.wustl.edu (Fritz Lehmann)
Message-id: <9409080359.AA02268@rodin.wustl.edu>
To: cg@cs.umn.edu, interlingua@isi.edu, srkb@cs.umbc.edu
Subject: International STANDARD FOR LOGIC: CSMF/CG/KIF
Cc: E.Hunt@cgsmtp.comdt.uscg.mil, bhacker@nara.gov, duschka@cs.stanford.edu,
genesereth@cs.stanford.edu, jksharp@sandia.gov,
msingh@bcr.cc.bellcore.com, msmith@vax2.cstp.umkc.edu,
roger@ci.deere.com, scott@ontek.com, sharadg@atc.boeing.com,
skperez@mcimail.com, sowa@turing.pacss.binghamton.edu, tony@ontek.com
Sender: owner-srkb@cs.umbc.edu
Precedence: bulk
INTERNATIONAL STANDARD FOR LOGIC:
CSMF - Conceptual Graphs - KIF (LONG)
Patrick Hayes (phayes@cs.uiuc.edu) wrote, answering me:
[Lehmann:]
>>...CCAT [the Peirce Project's Conceptual Catalogue and
>>Ontologies group] can, in addition, have ontologies expressed
>>in Conceptual Graphs which cannot be expressed
>>in current KIF (like "actors", Sowa-contexts, connected structures,
>>planarity, standard numbers, transitive closures, Buchi automata,
>>Montague grammars, power structures, Propositional Dynamic Logics,
>>etc.)[>>That is, CCAT could include more general Conceptual Graphs not
>>restricted to the KIF-equivalent IRDS Conceptual Graphs.]
[Hayes:]
>Well now, "cannot" is a very strong word. How many of these could be
>expressed as KIF ontologies, I wonder? (If you are going to point to the
>expressive wonders of higher-order logic, I will challenge you to show me
>how Sowa's CG's can quantify over relations and functions with enough
>frisson to eliminate nonstandard models of arithmetic.)
>By the way, this is the kind of reason why we need a model theory for CGs
>which is precise (and stable) enough to allow some metamathematics to
>actually be done.
>Best wishes
>Pat
Pat, I believe "cannot" is correct so long as the proposed
Knowledge Interchange Format (KIF) and the "IRDS" Conceptual Graphs
are limited to pseudo (i.e. First-Order schema-based) higher-order
Logic, as opposed to genuine, classical (any-order) logic including
quantification of all predicates and relations. This theory
difference has consequences.
The two logic languages KIF and Conceptual Graphs are being
considered by the ISO/IEC JTC1/SC21/WG3/CSMF Interim Committee
meeting next week in Seattle as potential languagues for an
INTERNATIONAL STANDARD FOR LOGIC in conceptual descriptions
("Conceptual Schema Modelling Facility" or "CSMF"), so now is a good
time to summarize the problems again. I fully support the quick
adoption of a logic standard for knowledge interchange, but the
standard should include classical logic ("strongly" higher-order,
with quantification over predicates, functions and relations) and not
limit the logic standards definition to "First-Orderism" (quantifying
only over individuals) unless there is a very good practical reason
given for it. "First-Order-Only" should be an _option_ (which would
include "weakly higher-order" schema-based or Henkin semantics) but
not a requirement.
Here briefly are _some_ of the troubling proved consequences of
First-Orderism. Instead of explaining them right here, I'll attach
at the end of this message y earlier list of 59 "Knowledge
Representation Examples Involving Some Potentially Higher-order
Notions" as an Appendix for references and background. I mailed that
Tech. Report to you a few months ago.
ANY FIRST-ORDER-ONLY-BASED LANGUAGE...
CANNOT DEFINE "CONNECTED" STRUCTURES - Connectivity is needed
for many practical applications, including electronics (and for the
concept of logical relevance as in Ben Kuipers' Access-Limited
Logic). This is like the limitation that single-layer perceptrons
had in the 1960's (as was pointed out by Minsky & Papert), which
almost destroyed neural net research until it was fixed.
Fundamental. Ehrenfeucht and Fraisse proved this result in the
1950's.
CANNOT DEFINE "PLANAR" GRAPHS - Ehrenfeucht-Fraisse again.
CANNOT DEFINE "EQUALITY"
CANNOT DEFINE ORDINARY NATURAL NUMBERS - it can only define
Non-Standard (Robinsonian) Numbers, using pseudo-Peano axioms. If I
ask a Knowledge Base, "How many integers are between 7 and 9,
inclusive?" I want it to answer "three: 7, 8, and 9.", but the First-
Order-based system's answer is: "An infinite number of mutually non-
isomorphic, nonstandard integers (including 'Robinsonian
infinitesimals')." Gee, thanks a lot.
CANNOT DEFINE "FINITE" OR "INFINITE"
CANNOT DEFINE HIGHER ORDER RELATIONS OF MONTAGUE GRAMMARS
CANNOT EXPRESS THAT ALL OF A CLASS OF FUNCTIONS OF x
HAVE A CERTAIN KIND OF VALUE - (e.g. "All monotonic
functions of 42 have positive values.")
CANNOT DEFINE TREES (AS OPPOSED TO CYCLIC GRAPHS OR FORESTS)
CANNOT SAY "ANY TWO THINGS MUST DIFFER IN SOME QUALITY"
CANNOT DEFINE "TRANSITIVE CLOSURE" RELATION - (e.g. of
Ancestor to Parent)
CANNOT DEFINE "COUNTABLE"
CANNOT DEFINE "INCHOATIVE" SYSTEMS, and
NO DECLARATIVE SEMANTICS FOR PROGRAMS
OR PROCEDURES IS POSSIBLE. To do this, some system like
Denotional Semantics of Dana Scott and Christopher Strachey, or
Propositional Dynamic Logic of Vaughan Pratt, M. Fischer & R. Ladner,
is needed. These are strongly higher order.
FOR MANY MORE, SEE ATTACHED APPENDIX.
It is hard to imagine that any language with these known
limitations would be adopted as an official international or government
standard for _general_ logical descriptions and definitions. As a
particular SUB-language option, it may be appropriate for limited finite
domains.
Having pointed out some mathematically proved defects of "First-
Orderism", let me note the reasons given so far _for_ the First-Order
approach. First the technical difference: A First-Order schema-based
mock-up of higher-order logic is "complete" (every true theorem is
First-Order derivable), "compact" (everything true of the finite subsets
of any infinite set must be true of the whole set) and "Lowenheim-
Skolem" (similar, for transfinites); genuine higher-order logic is not.
Some logicians who admire completeness, compactness, and Lowenheim-
Skolem-ness are willing to put up with the very peculiar consequences
and limitations of First-Orderism. Other logicians, including probably
all advanced model-theoretic logicians, are not willing to put up with
it. Joe Six-Pack Knowledge Base User wouldn't put up with it either if
he were told about the bizarre consequences.
You said the KIF committee at AAAI-94 had decided to stick with
First-Orderism not so much for any theoretical reasons, but because
"higher-order unification can get messy." This is an inference-
implementation issue, which is inappropriate as the decisive factor in
creating a universal logic standard. (People around the world are in
fact working on practical higher-order unification.) You personally
defended _completeness_ as a philosophically desirable feature although
you adduced no practical benefits of completeness, and you apparently
prefer the resulting Non-Standard (Robinsonian) Numbers to standard
natural numbers. Mike Genesereth, whose "baby" KIF is, declined to
respond to these logical criticisms of KIF for months, other than one
terse note asking what the problem was. John Sowa, whose "baby"
Conceptual Graphs are, did give conscientious and thoughtful responses,
as you did. Whereas you like completeness, Sowa likes _compactness_,
which he defended at ICCS-94 on aesthetic rather than practical grounds.
A year ago I challenged you (as head of the KIF "logical
foundations" group) to add to that group some advanced logicians and
model-theoreticians who actually understand higher order logic and model
theory, and I mentioned some names. This you did not do. It's not
unfair to say: no-one associated with KIF has exhibited any knowledge of
the subject (in the email discussion at least).
Pat, to answer your specific questions:
>>...[CCAT can use concepts that] cannot be expressed
>>in current KIF (like "actors", Sowa-contexts, connected structures,
>>planarity, standard numbers, transitive closures, Buchi automata,
>>Montague grammars, power structures, Propositional Dynamic Logics,
>>etc.)[>>That is, CCAT could include more general Conceptual Graphs not
>>restricted to the KIF-equivalent IRDS Conceptual Graphs.]
>Well now, "cannot" is a very strong word. How many of these could be
>expressed as KIF ontologies, I wonder?
Unless I am mistaken, none. "Actors" in Conceptual Graphs are
procedural. Genesereth has stated often that KIF is declarative and not
procedural. To provide declarative semantics for procedures requires
correct treatment of recursive functions, functions of functions, and
programs which loop infinitely and never halt; this requires "reflexive"
algebraic structures of partial functions like the continuous lattices
of Dana Scott, which leads to domain theory and necessary distinctions
which are strongly higher-order. Other approaches like Propositional
Dynamic Logic also require strongly higher-order definitions. Some
purely First-Order declarative semantics that works for programs may
exist, but I am not familiar with any.
By "Sowa-contexts" I mean the algebraic structure of the nested
contexts in a Conceptual Graph. Remember that Sowa told you and me at
ICCS-94 that he would allow nesting (full inclusion) of contexts on a
single "sheet of assertion" but not partially overlapping contexts.
Such a system of nested regions is isomorphic to a rooted tree. The
class of rooted trees is not First-Order definable, so Sowas's
"contexts" could not be defined. (Partially overlapping contexts would
change the equivalent tree to a DAG with circuits. If no "outer"
context is designated as sheet of assertion, the tree is not rooted nor
necessarily connected.)
The rest of the examples listed above occur in the Appendix below
as proven strongly higher-order constructs.
>(If you are going to point to the
>expressive wonders of higher-order logic, I will challenge you to show
me
>how Sowa's CG's can quantify over relations and functions with enough
>frisson to eliminate nonstandard models of arithmetic.)
Sowa's "IRDS" or "standards" Conceptual Graphs are supposed to
share KIF's formal semantics, so unless they take numbers as primitives
they are stuck with Nonstandard Nmbers. Regular CGs do not necessarily
attempt to define natural numbers in terms of First-Order Logic (pseudo-
Peano with schemas); Sowa has said that the natural numbers may be given
as primitives. I support this completely. The CCAT group deals with
ontologies. Whether CCAT's CG ontologies can eliminate nonstandard
models is itself determined by ontology at the deep level (even model
theory must have its own ontology). Sowa has approvingly quoted Quine:
"To be is to be the value of a quantified variable" (approx. quote).
Choosing an ontology includes choosing what may quantified over. An
ontology may permit quantifying over all predicates and relations, and
hence be strongly higher-order, hence eliminating non-standard models of
the numbers. Sowa does not do so himself, because he likes compactness;
instead, like you, he uses the First-Order axiom-schema kludge for
higher-order relations. He can avoid Nonstandard Numbers even so, by
just taking natural numbers as primitives. In a knowledge-sharing
language for practical use, nobody except the really hard-core First-
Orderists (and maybe you?) will ever _want_ to be stuck with Numbers instead of natural numbers.
>By the way, this is the kind of reason why we need a model theory for CGs
>which is precise (and stable) enough to allow some metamathematics to
>actually be done.
By the way, this is the kind of statement which misleads people as to
supposed formal differences between KIF and Conceptual Graphs. Conceptual
Graphs have always had a model theory based on Sowa's "phi" operator which
transformed them into First-Order logic. Some parts of Sowa's broader
theories were excluded, but most of these now have full model-theoretic
semantics. After a year-long hiatus, you recently have resumed conjuring up
the allegedly "unusual" or "unconventional" semantics of CGs. (I don't
remember your exact words.) There's nothing unconventional or even
interesting about CG's formal semantics. Its only peculiarity is the
limitation of Sowa's standard CGs to schema-based First-Orderism which you
and KIF share! Now and then Sowa seems tempted to bring "situation theory"
into the formal logic (as opposed to the ontology), but I hope to have
dissuaded him at ICCS-94. Remember that you and I logically jabbed and
stabbed at Sowa for several hours (I even more than you). Except for the
"situations" (and subsumption between relations of different arities, a
question for KIF too if it has typed defined relations), Sowa either
answered every criticism or retreated into the safe zone. The model theory
of CG's has been more "precise (and stable)" than that of most competing
Knowledge Representation formalisms. CGs never traipsed down the
nonmonotonic logic trail, for one thing. I'm glad KIF has now stepped back
out of it.
I wish the Standards Committees could obtain a balanced and
_informed_ briefing on the logic-order issue.
Yours truly, Fritz Lehmann
GRANDAI Software, 4282 Sandburg Way, Irvine, CA 92715, U.S.A.
Tel:(714)-733-0566 Fax:(714)-733-0506 fritz@rodin.wustl.edu
=============================================================
A P P E N D I X: TR-93-4
Knowledge Representation Examples Involving
Some Potentially Higher-order Notions
====================================================
LIST OF POTENTIALLY HIGHER-ORDER CONCEPTS MENTIONED IN
H-O KIF/CONCEPTUAL GRAPHS THREAD SINCE SEPTEMBER 1993.
I've been asked by a few people to re-list my "about five
or six" earlier email examples which might call for higher-
order treatment. Actually it's closer to 50 examples by now,
though not all are good test cases. Since I started this
thread in September, I've mentioned the following examples as
being at least potentially higher-order. Not all of these
require strongly higher-order formal semantics. Some do
(especially the later ones). The rest can be handled with
(varying degrees of) "syntactic sugar". When this is possible
can be a subtle question. Fritz Lehmann, Nov. 1993
1. "Aristotle has all the virtues of a philosopher."
[possibly taken by C.S.Peirce fom Mediaeval example]
Try: "AP((Virtue(P) & Ax(Phil(x)->P(x))) -> P(Aristotle))"
2. Patrick Winston's relation-between-relations semantic net
link [between the "left-of" and "right-of" relational links
in his block-arch diagrams].
3. The IS-A link in inheritance and subsumption hierarchies.
[as a transitive relation or link, not a set of FO axioms]
4. The relational IS-A/subsumption link in relational
hierarchies. [some arguments may be permuted!]
5. The formal definition of individual identity or equality.
[As in "x = y =def= AP(P(x) iff P(y)). Leibniz]
6. The assertion that, for a particular individual, all of a
certain kind of functions on that individual take a certain
kind of value. [including recursively defined functions]
7. The ability to refer to and predicate the relations which
exist between a given relation and its own arguments. For
R(a,b), this yields R'(a,R); R''(b,R,R'); and infinitely more.
[one kind of hypostatic abstraction of relations into objects]
8. Semantic "case relation" taxonomy links.
[see 4, & Parker-Rhodes, "Inferential Semantics", 1978, p. 235]
10. The inclusion ordering in cylindric algebras.
[see 4. Merry-go-round problem? "C.A.s" Henkin, Monk & Tarski 1971/85]
11. The type lattice on Conceptual Graphs relations [circles].
[see 4, Sowa "Conceptual Structures" 1984 mentions only slightly]
12. Closure of the universe under classes and disjoint unions
of direct products. [my domain allowing n-order poly-arity rel.s]
13. Harold Boley's Directed Recursive Labelnode Hypergraphs
[under closure, see his art.in my "Semantic Networks" 1992, p.601].
14. The meanings of, and explicit relations among, the
"columns" of a [relational] database.
15. Relations in hierarchies of Rudolf Wille's Concept
Lattices. [see his art. in my "Semantic Networks" 1992, p.493]
16. In Euclidean Between(a,b,c), the qualities of a's relation
to the betweenness lacked by b's and c's [relations to the
betweenness].
17. The semantics of the named [perhaps semantically indexed,
and predicable] "argument positions" of any relation in Jim
Fulton's Semantic Unification Meta-Model (SUMM).
18. (In Conceptual Graphs) For some individual x in D, some
reified [PREDICATE: p] or [TYPE: p] in D, and assertion P(x), ---
what are Sowa's formal model-theoretic semantics that would let us know
that p=P?
19. In Tom Gruber's Ontolingua, the formal semantics of second-
order relations. The formal semantic difference, if any,
between (type Tx) and (chair Tx).
20. Peirce's "hypostatic abstraction" or reifying relations
into individuals, but retaining their essential relational
character.
21. "North is the opposite of South" [the point here being the
"opposite", not some converseness axioms about directions]
22. "The thief is to robbery what the beloved is to love."
[i.e. each individual stands in the same kind of relation to
the respective (different) relations.]
23. "Bart has all the virtues of a philosopher." [Similar in
form, if not truth value, to example no. 1]
[24]. [PAT HAYES' EXAMPLE] Beta-reduction of lambda sentences,
the form being "(lambda x.PHI[x]) (t) IFF PHI(t) for any WFF
PHI and term t". Hayes' example: "(lambda x. (IF (Exists y)(Rx,y)
THEN f(x)=f(f(x)) )) (g(a)) if R(g(a),b) then
f(g(a))=f(f(g(a))). Used a lot in HOL theorem provers.
25. Peirce's (or Leibniz's) sentence "Given any two things,
there is some character which one posseses and the other does
not." [Needed to distinguish among differing "individual
distinctness" criteria of different knowledge bases.
Distinctness of individuals not to be assumed already (in the
formal interpretation of this sentence). Appeared as
Fig. 80 in "The Existential Graphs" by D.D.Roberts
in my "Semantic Networks" 1992, on p.661 illustrating "Gamma" EGs.
I proposed "Ax,y(~(x=y)-> EP((P(x)&~P(y)) v (P(y)&~P(x))))" ]
[26]. [PAT HAYES' EXAMPLE?] Real number line without non-
standard models. [FO can't specify this?.]
27. Being able to mention 100 senators without having to list
4,950 explicit inequalities between pairs of senators, as in
FOL. [If 'sugared', the sugar has to be pretty strong.
Semantics should cover the _general_ case of n]
28. Defining equality formally by schema of FOL sentences on
finite vocabulary of Relations X No. of Argument-places, when
some relations have no fixed arities. [My answer to Hayes'
answer to no. 5.]
29. The [ever-present] relation in Category Theory between a
natural transformation and the relation between an affected
morphism and one of its participating objects.
30. Ontek Inc.'s 3rd and 4th order predicates. [big chart.
beyond Aristotelian "categories"?]
31. "All monotonic functions of 42 have positive values."
[Seems mundane, but don't neglect the recursive weirdos.]
32. Relations defined on connectives, as in work of Zellweger,
Menger or Stern. [Not sure logic-order is the issue here.]
[33]. [DAN SCHWARTZ'S EXAMPLE] Combination of classical outer
logic with fuzzy inner logic. [This initially strikes me as a
meta-level issue rather than a logic-order issue.]
[34]. [DAN SCHWARTZ'S EXAMPLE] Combination of quantification,
likelihood, and usuality. [Same comment.]
35. Formalizing distinction among First-Order/set-based,
higher-order/approximative/intensional, and inchoative systems.
[See example 25 above which is: logically-true theorem in
finite boolean algebra of monadic preds; contingent axiom in
intensional, approximative and HOL; false in inchoative systems
(see Parker-Rhodes "Theory of Indistiguishables", Reidel, 1981)]
36. Formalizing higher-order factorizations of large-scale
structure of concept hierarchy. [e.g. poset actors via
my "skeleton products" and "fret products" of order-sorted
relational graphs and sort posets. Determinables as factors.]
37. Formal semantic definition of the predicate "infinite".
[Strongly higher-order. Barwise, in Barwise & Feferman, 1985,
and many others.]
38. Formal semantic definition of "countable sets".
[Strongly higher-order. Barwise, in Barwise & Feferman, 1985]
39. Formal semantic definition of "well-orderings".
[Strongly higher-order. Barwise, in Barwise & Feferman, 1985]
40. Formal semantic definition of "natural numbers".
[Strongly higher-order. Last Peano axiom has AP (induction).]
41. Formal semantic definition of "real numbers".
[Strongly higher-order. Barwise, in Barwise & Feferman, 1985]
42. Formal semantic definition of the classifying properties of
ordered Abelian groups.[Strongly higher-order. Various authors
in Barwise & Feferman, 1985]
43. Formal semantic definition of the classifying properties of
various kinds of automata. [incl. Buchi.Strongly higher-order.
Gurevitch in Barwise & Feferman, 1985]
44. Formal semantic definition of the classifying properties of
classes of [potentially infinite] trees.
45. Formal semantic definition of topological, compact and
Hausdorff spaces.[Strongly higher-order. Dickmann,
in Barwise & Feferman, 1985]
46. Formal semantic definition of the classifying properties of
complete partial and linear orders, lattices, and Boolean
algebras.[Strongly higher-order. Dickmann,
in Barwise & Feferman, 1985. Includes "CPO"s]
47. Formal semantic definition of the classifying properties of
Scott-type domains. ["topped" incl. in 46. Strongly higher-order.
Scott-type domains are the basis for Denotational
Semantics for programs and procedures. See also Vienna Semantics,
Dynamic Logic Semantics, Intensional Program Semantics, Various
Algebraic and Categorial Semantics, etc.]
48. Formal semantic definition of the classifying properties of
various kinds of probabilistic systems. [ Strongly higher-order.
incl. probabilistic quantifiers. Keisler 1985].
[49]. [MARK GRAVES' EXAMPLE] Inter-relation relations in genome
mapping. Powered vector of "distance" notions used to classify.
[50]. [PAT HAYES' EXAMPLE] Second-, third- (and fourth-?) order
constructs in Montague Grammars.
51. The PDES/STEP EXPRESS industrial language including its
procedural attachment features. [latter require program semantics as
in 47. EXPRESS manual, Peter Wilson]
52. Extended temporal logics, e.g that of Wolper, or Kozen's mu-
calculus. [Stirling in "Handbook of Logic in Comp Sci", v2,
Abramsky, Ed., Oxford U. Press, 1992. Strongly higher order.]
53. Propositional Dynamic Logics of Pratt and Kozen, Fischer &
Ladner. Includes higher-order axioms. [Same. Strongly higher order.]
54. The concept of connectivity of finite graphs. [Strongly higher order]
55. The concept of planarity of finite graphs. [Strongly higher order]
To justify 54 and 55 I quote: "Originally, Ehrenfeucht-Fraisse
games were used to prove that certain concepts are not definable by
first order formulas even if restricted to finite structures. Among
such concepts we find connectivity and planarity of graphs." J. A.
Makowsky, Model Theory and Computer Science, in v. I, Handbook of
Logic in Computer Science, S. Abramsky et al., Ed.s, Oxford U.
Press, 1992, p. 779. If KIF and CGs really can't even define finite
connectivity, then I forsee trouble ahead. I'm reminded of what the
same limitation of single-layer perceptrons did for neural network
research in the 1970's after Minsky & Papert's expose'.
56. Complex algebras. [in Universal Algebra. See Gratzer et al.]
57. Chris Brink's Power Structures [powering of dyadic reltios,
between individuals to dyadic relations between sets of indiv.s. See
article in Algebra Universalis recently/forthcoming? Related to
Hoare, Smyth, Egli-Milner/Plotkin powerdomains.]
58. The refinement order on set partitions. [this order relation
is 2nd order on equivalence relations]
59. [MATT GINSBERG'S EXAMPLE] The definition of a relation A as the
transitive closure of a relation B. C.f. the definition of "transitive
closure" itself.
==========================
This list could be shortened considerably by
removing some examples which are essentially
duplicates and those which can simply be handled
correctly in First-Order logic. One could add
more candidate examples too.
Fritz Lehmann fritz@rodin.wustl.edu
REFERENCES
S. Abramsky, D. Gabay & T. S. E. Maibaum, Handbook of Logic in
Computer Science, Oxford Univ. Press, Oxford, 1992.
J. Barwise & S. Feferman, Ed.s, Model-Theoretic Logics, Springer,
Berlin, 1985.
G. Gratzer, Universal Algebra, 2nd Ed., Springer, Berlin, 1979.
L. Henkin, J. D. Monk & A. Tarski, Ed.s, Cylindric Algebras, Vol. I &
II, North-Holland, Amsterdam, 1971;1985.
Wilfrid Hodges, Model Theory, Cambridge University Press, 1993.
F. Lehmann, Ed., Semantic Networks in Artificial Intelligence,
Pergamon Press, Oxford, 1992.
M. Minsky & S. Papert, Perceptrons, MIT Press, 1969;1988.
A. F. Parker-Rhodes, Inferential Semantics, Humanities/Harvester
Press, Atlantic Highlands, NJ/Hassox, Sussex, 1978.
A. F. Parker-Rhodes, The Theory of Indistinguishables, Reidel,
Dordecht, Holland, 1982.
J. Sowa, Conceptual Structures, Addison-Wesley, Reading, Mass., 1984