Higher-Order KIF & Conceptual Graphs
FWLIV@delphi.com
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
=====================================