**Mail folder:**Interlingua Mail**Next message:**Tom Gruber: "Re: Ontologies and theories"**Previous message:**Christopher P Menzel : "Re: Ontologies and Theories"

Message-id: <199208242010.AA14418@venera.isi.edu> Date: Mon, 24 Aug 92 16:04:07 EDT From: sowa@watson.ibm.com To: SRKB@ISI.EDU, INTERLINGUA@ISI.EDU, CG@CS.UMN.EDU Subject: Types, sorts, vocabularies, theories, and ontologies

Some comments on Chris Menzel's comments (marked by >) and John McCarthy's comments (marked by >>): >> 1. F = ma was proposed as a definition of force by Ernst Mach. >> I don't think he was right to do so, but it can be done. That's true. But this is a typical example of a relationship among three different quantities, and it is rather arbitrary to take it as a definition of any one of the three. I would prefer to put it in the collection of axioms for the theory. >> The point is that what is a definition >> and what is a law is dependent on the current state of science. >> KIF should also allow this flexibility. I agree, and I would therefore like to have two separate pots for storing the definitions and the laws. >> 2. The mathematicians do use logics that distinguish what computer >> scientists call types. They call them sorts and refer to multi-sorted >> logics. The word "type" is used for the positions in the hierarchy of >> predicates and functions whose arguments are predicates and functions. >> It is regrettable that the word "type" was taken into computer science >> by people who didn't trouble to look it up. The problem is that >> computer science needs both sorts and types in the mathematical sense. >> It would be good if KIF were to use the mathematicians' terminology >> since it suits computer science better than what has become customary >> in computer science. > Very true, only things aren't *quite* as tidy as John suggests. Even > among logicians `type' is a bit of a weasel word. Modern usage of > course begins with Russell's simple theory of types, his first go at > circumventing the logical paradoxes, initially in the {\it Principles > of Mathematics} in 1903. In the simple theory, types are essentially > classes of similar objects: the lowest type is the class of all > individuals, the next the class of all classes of individuals, and so > on. The simple theory is thus most naturally taken to be extensional. > (Though this would have to be qualified.) I sympathize with both John and Chris. In my first published paper on conceptual graphs in 1976, I used the term "sort label" for the things that I put on the left side of the concept boxes. But I quickly learned that to a programmer, the word "sort" has one very strong association: the process of putting things in alphabetical order. For all practical purposes, the people who are familiar with Russell's theory of types are a set of measure zero. Furthermore, the term "type" as used in computer science is broad enough to include the meanings of both "sort" and Russell's notion of "type". I would also like to comment on Chris's phrase "Modern usage of course begins with Russell...." I admit that Bertrand Russell was a very smart man, but he also made some dumb choices. One of the dumbest was his choice of C. S. Peirce's 1883 notation for predicate calculus instead of Peirce's 1896 notation for existential graphs. Along with that choice of notation, Russell presented the world's worst proof procedure in the Principia Mathematica. In another note, I'll send an example of a proof of Proposition 3.47, which can be proved in Peirce's system in 8 steps starting from a blank sheet of paper. But Russell takes 43 inference steps with 28 citations of other propositions scattered all over the first 3 chapters of the Principia. Yet Peirce published his rules of inference 13 years before the Principia and 37 years before Gentzen's system of natural deduction (which is a special case of Peirce's rules). > Also, it might be pointed out that first-order multi-sorted logics, > while often a great convenience, are no stronger than plain vanilla > first-order logic. Hence, there is no *theoretical* reason for > introducing sorts into KIF, especially given the intended purpose of > the "frame ontology" that Tom Gruber posted a couple of days ago. > Sorts can be introduced as needed by a suitable mechanism. One might just as well say there is no *theoretical* reason for any programming language beyond a Turing machine. My response is to quote a little passage from a letter by Carl Friedrich Gauss: All new systems of notation are such that one can accomplish nothing by means of them which would not also be accomplished without them; but the advantage is that when such a system of notation corresponds to the innermost essence of frequently occurring needs, one can solve the problems belonging in that category, indeed one can mechanically solve them in cases so complicated that without such an aid even the genius becomes powerless. Thus it is with the invention of calculating by letters in general; thus is was with the differential calculus.... To paraphrase Gauss, types or sorts are "frequently occurring needs" that are used in almost every knowledge representation language. Every system of ontology needs them. They simplify the statement of formulas in predicate calculus. They make it easier to translate between two different systems with types, and they do nothing to hinder translations between systems without types. When I cornered Fikes and Genesereth last March, they agreed that types could easily be added to KIF. Please don't let them wriggle out of that commitment. >> 3. The dictionary and philosophical usage use "ontology" to refer to >> what exists. In the old days there were arguments about the existence >> of various things. Quine made the term technical, saying that the >> ontology of a theory is the correspondence between variables in the >> theory and the domains in which they take their values. Roughly >> then, the ontology of a theory is given by the kinds of things assumed >> to exist over which the variables can range. > Not just the kinds of things, but the particular things as well, > though this point gets buried in Quine's aversion to individual > constants in favor of predicates like `Socratizes'. But if I > introduce a name into my logic, and say some interesting things using > that name, then (assuming I'm not a so-called "free" logician) there > must be something in my ontology that it denotes. I don't disagree with these two points. But my main contention was that we have two very nice words in English that are more widely known and more accurately used by most people than the word "ontology": namely, "vocabulary" and "theory". I suggest that we use the word "vocabulary" for the collection of terms and definitions, and "theory" for the triple (Language, Vocabulary, Axioms). I would prefer to limit the word "ontology" to metaphysical discussions where people are explicitly analyzing the relationship between their vocabulary and the things in the real world. People might have to assume an ontology before writing down their vocabulary, but what gets stored in the computer are vocabularies and theories, not ontologies. John Sowa