**Mail folder:**Interlingua Mail**Next message:**phayes@cs.uiuc.edu: "attitudes to Krep"**Previous message:**Varol Akman: "integers"**In-reply-to:**Fritz Lehmann: "Higher-order KIF & Conceptual Graphs"**Reply:**Fritz Lehmann: "Higher-order KIF & Conceptual Graphs"**Reply:**david l. martin: "Re: Higher-order KIF & Conceptual Graphs"

Reply-To: cg@cs.umn.edu Date: Sat, 20 Nov 1993 13:59:19 -0400 (EDT) From: FWLIV@delphi.com Subject: Higher-Order KIF & Conceptual Graphs To: interlingua@isi.edu, cg@cs.umn.edu, boley@dfki.uni-kl.de, phayes@cs.uiuc.edu Message-id: <01H5JH8WXZWY8ZESCL@delphi.com> X-Vms-To: INTERNET"interlingua@isi.edu,cg@cs.umn.edu,boley@dfki.uni-kl.de,phayes@cs.uiuc.edu" Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Transfer-Encoding: 7BIT

PAT HAYES SAID> > There are two different semantic stories that can be told about > higher-order predicate syntax. According to one - the classical one - the > quantifiers range over ALL functions, relations, etc., that is, all > uncountably many of them. According to the other - Henkin's model theory - > they may range over some subset of these uncountable sets (but not any old > subset; the ranges must at least contain a referent for each function, > predicate etc. which is definable in the language). It is the SAME language > in each case, with the SAME inference rules, but different semantic > accounts are being given of it. > According to the classical story the logic is incomplete and according to > Henkin's story it is complete, which is just another way of saying that > Henkin's account is accurate and the classical story is not. Pat's use of "classical".nicely conforms to my original remark (re Jim Fulton's phrase "classical logic") which started this whole thread: "classical logic" does not mean First-Order Logic (FOL); it is n-order and FOL is just one of its many possible sublanguages. If KIF and Conceptual Graphs were to be limited to employing FOL-reductions of the real thing which depend on arbitrary syntactic assumptions about some available vocabulary (and arities) of relation-symbols ("referents" above), then they wouldn't be based on classical logic. After all my efforts to get the First-Orderists to say for once why completeness (or compactness) is actually good or relevant (in Knowledge Interchange practice), Pat says that the FOL mock-up is "accurate" and classical logic is not. Why "accurate"? When Joe KR-User declares simply that "All monotonic functions of 42 have positive values" he means it, and it is not "accurate" to say he really means only certain monotonic functions which happen to be FOL-definable. The fact that we may not be able to compute all of them in finite time is irrelevant -- and the fact that functions like Pat's concept "VERY BIG" are included is also no problem if it's a given that they're monotonic functions. Joe KR-User still really means ALL monotonic functions (and he's incidentally quite right) and anything else looks to me more "inaccurate". CHRIS MENZEL, ANSWERING HAYES ABOVE< <Wellll, depends on what the target is, doesn't it, Pat? For those not <skeptical of the power set operation (a scorned minority, perhaps, in <this crowd), the intended semantic target of "true" higher-order logic <*is* the full higher-order universe of *all* (bang the table, stamp the <foot) functions, relations, etc., and so it is Henkin's story that is <inaccurate and the classical one that gets it right. Incompleteness <(on this view) is then just the cost of getting it right. < Regards, --Chris This is correct; I'll withold comment on power-set skepticism. I still haven't heard of any practical reason for forcing a knowledge representation user to adopt the First-Order-istic approximation, and it may be that there are practical reasons for not doing so (if among our 50+ potential examples there are practical uses for those concepts which are strongly higher-order definable but not weakly so). Perhaps for some users the "FOL-inaccessible" functions and relations in classical logic will have a role in Knowledge Rep. like that of imaginary complex numbers in engineering. They are used for intermediate results but not for the final values which must be reals. You map from an accessible domain-model to an abstract one with certain desirable structural characteristics, perform valid transformations there, and then you map back to the accessible domain-model for the usable results. This proves to be very useful in engineering even though you can't actually measure any imaginary lengths or cardinalities of real-world objects. (Formal semantics for procedures/programs might be one application of this principle; one program can be shown to subsume another even if for some inputs neither program ever halts in "accessible" time.) I asked a very prominent logician about this email debate. He declined to join the fray, so I won't name him, but I'll quote this: "Fritz, I got tired of fighting first-order-itis... There is no convincing the die-hard first-order-ite. It is too easy to spend hours debating to no purpose at all." Evidently these waters have been well- explored before by the real model-theoreticians. PAT HAYES SAID> >By the way, I haven't seen your interesting sounding list of examples. >Is it available by email? It's just the 50+ potentially HOL concepts mentioned so far in this thread; I sent a list of the first 49 to interlingua and cg, followed by a few additions. I'll append an updated version to the end of this message. Yours truly, Fritz Lehmann fritz@rodin.wustl.edu 4282 Sandburg, Irvine, CA 92715 USA 714-733-0566 ==================================================== 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/intesional, 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 factors 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 relations, between individuals to dyadic relations between sets of indiv.s. See article in Algebra Universalis recently/forthcoming? Related to Hoare, Smyth, Egli-Milner powerdomains.] 58. The refinement order on set partitions. [this order relation is 2nd order on equivalence relations] ===================================== This list may be reduced considerably by removing examples which are essentially duplicates and those easily handled by (a finite no. of) First-Order sentences. Also, more can be added. Fritz Lehmann fritz@rodin.wustl.edu =====================================