Higher-order KIF & Conceptual Graphsfritz@rodin.wustl.edu (Fritz Lehmann)
Date: Fri, 21 Jan 94 05:04:33 CST
From: email@example.com (Fritz Lehmann)
To: firstname.lastname@example.org, interlingua@ISI.EDU, email@example.com
Subject: Higher-order KIF & Conceptual Graphs
The "logical foundations" KIF committee which Pat Hayes is
to head should have some balance, if it is to properly address
the issue of whether to use real, classical higher-order semantics,
or just a schema-based First-Order imitation for the sake of
completeness and compactness. Pat himself, although he first
raised the higher-order question some months ago, seems to have
come very firmly down on the side of First-Orderism (partly based
on his demand for completeness for full "logical grounding"). If
the rest of the committee consists only of other KIF-ites who
originally voted for First-Orderism in the first place, the
imprimatur of the committee will mean little. (Echoes of Matt
Ginsberg?) Specifically, there should be some people with actual
higher-order logic (and model theory) expertise, or the committee
might be as uninformed on this issue as is customary. Someone
should actually understand the work of Fraisse, Ehrenfeucht,
Shelah et al. I suggest asking people like Samson
Abramsky, J. A. Makowsky, Jon Barwise, Dana Scott, G. P. Huet,
Solomon Feferman, Wilfred Hodges, or Y. Gurevitch to recommend
some knowledgeable people willing to be committee members.
Also the committee might initially address our earlier
"Hayes/Lehmann dichotomy" between a system with only fully
logically interpreted predicates, for an entire agent's
"semantics", and a system combining logically interpreted
predicates with "primitive" predicates (like Hayes' "VERY-BIG")
interpretable only outside the system, for practical knowledge
I surmise that Conceptual Graphs' formal semantics will
mainly be in John Sowa's hands (except to the extent that he might
elect to defer to the KIF committee). He was spirited in his
defense of a particular brand of First-Orderism which excludes
numbers from the model-theoretic semantics and takes them as a
kind of semantic primitive. (I personally totally agree with the
latter decision, even with full classical semantics available.)
Yours truly, Fritz Lehmann
4282 Sandburg, Irvine, CA 92715 USA 714-733-0566
P.S. I notice extensive use of higher-order unification and
equational matching in "The Clausal Theory of Types" by D. A.
Wolfram, Cambridge University Press, 1993, including Third-Order.
P.P.S. Must we totally neglect intension? Sinn? Two facts
are: A. There are too many different discordant notions of
what "intensions" are and many are hard to formalize neatly,
whereas everybody pretty much understands extensions as a formalism.
B. Notwithstanding fact A., intensions really matter more than
extensions. Triangularity is the thing to know about, not the set of
triangles. Same goes for Democracy, puffinhood and FAX machines.
Who really cares about arbitrary extensional sets of objects?
Extensional logic is neat and easy, but it's just a constraint on
the logic that matters. Pegasus is not a golden mountain,
for one thing, even if their empty extensions are the same.
This is a big issue for Knowledge Representation, or should be.