Types, sorts, vocabularies, theories, and ontologies

sowa@watson.ibm.com
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