**Mail folder:**SRKB Mail**Next message:**Chris Menzel: "Re: International STANDARD FOR LOGIC: CSMF/CG/KIF"**Previous message:**Pat Hayes: "Re: CCAT Conceptual Catalogue and Ontologies"**Reply:**Chris Menzel: "Re: International STANDARD FOR LOGIC: CSMF/CG/KIF"

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