Re: Ontologies and Theories

• Mail folder: SRKB Mail
• Next message: sowa@watson.ibm.com: "Types, sorts, vocabularies, theories, and ontologies"
• Previous message: John McCarthy: "Ontologies and theories"
• Maybe in reply to: John McCarthy: "Ontologies and theories"

From: Christopher P Menzel          <cmenzel@tamsun.tamu.edu>
Message-id: <9208222201.AA04268@tamsun.tamu.edu>
Subject: Re: Ontologies and Theories
To: interlingua@ISI.EDU, srkb@ISI.EDU
Date: Sat, 22 Aug 92 17:01:01 CDT
X-Mailer: ELM [version 2.3 PL11]

John McCarthy writes:

> 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.)

Things changed a lot when Russell moved to the *ramified* theory of
types in an ill-fated attempt to solve the semantical paradoxes like
the liar as well as the logical paradoxes.  In the ramified theory,
the elements of higher types are now best taken to be *intensional*
entities, full blown properties and relations ("propositional
functions" in Russell's jargon), though there is great confusion in
Russell's writings on this point between syntax and semantics.  At
certain points he appears to assign types to formulas with free
variables, and at others to propositions and propositional functions
in such a way that he cannot be understood syntactically.  On the
ramified theory, each type is partitioned into a system of *orders*,
where a propositional function's order is determined both by the
orders of its arguments and by the orders of the entities it (or more
exactly, the expression that denotes it) quantifies over.  This
prevents the sort of "vicious circularity" that Russell, Poincare, and
others took to be the culprit behind all forms of paradox generally.
(Confusingly, what is called higher-order logic these days is usually
just a form of simple type theory, which had no notion of order.)

Later systems of type theory, notably those of Church and Montague,
understand types first and foremost to apply to syntactic entities.
Thus, in Montague's least complicated type theory, e is the type of
individual expressions, t is the type of truth-value denoting
expressions (sentences, roughly), and if a and b are types, (a,b) is
the type of an expression that, when applied to an expression of type
a, yields an expression of type b.  Thus, a one-place predicate is of
type (e,t), since applied to an individual term the result is a
sentence.  His intensional type theory is just a variation on this
theme.  Generally speaking, of course, one can define an analogous
notion of *semantic* type.  E.g., for a Montague-style semantics,
individuals are of type E, truth values of type T, and functions from
entities of type A to entities of type B are of type (A,B).

It should be noted that there are type-free theories of intensional
entities in the marketplace as well, and powerful arguments for
preferring them to typed theories in certain contexts, at least.

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.

I will defer to McCarthy about the need for higher types in computer
science per se, but it is not clear to me that KIF needs them.  This
is worth discussing.  John Sowa and I had a brief exchange that
addressed some of the relevant issues which I *think* got cross-posted
to Interlingua a few months back.

> 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.

> This usage is also
> more appropriate for computer science than the fuzziness of current
> computer science usage.

Not to mention the broader worlds of information modeling and
"enterprise engineering."

--Chris Menzel