I had some offline discussions on this topic that may help
clarify various issues in this thread. (01)
One topic is the terminology about 'sort' and 'type', which
are frequently used in ways that are sometimes synonymous,
sometimes distinct, and sometimes ambiguous. (02)
Bertrand Russell adopted the general English word 'type' for
a highly specialized use: the domain of individuals in some
model (first order quantifiers range over that set), the set
of all possible relations among those individuals (the domain
of second-order quantifiers), the set of all possible relations
of relations (the domain of third order quantifiers), and so on... (03)
Because of the prestige of the _Principia Mathematica_, other
logicians avoided using the word 'type' for other kinds of
classifications. Instead, some adopted the word 'sort' instead
of 'type' for a way of classifying the kinds of things in the
domain of quantification. (04)
I received an offline email note criticizing my vacillation
between the words 'sort' and 'type' in conceptual graphs.
In my first published paper about CGs, I followed the logicians
in using the word 'sort': (05)
http://www.jfsowa.com/pubs/cg1976.pdf
Conceptual graphs for a database interface (06)
But the programming language community adopted the word 'type'
for datatypes. That was a natural choice for them. In the 1970s
and early '80s, I worked with Ted Codd and other DB people, and
I realized that the word 'sort' was a non-starter in the DB and
programming community. It also conflicted with terminology in
linguistics. I had to make a choice, and I decided to use the
general term 'type' to include both Russell's usage and the
common usage in other fields -- especially programming languages. (07)
For an overview of sorted logic and related issues, I recommend
the following collection of papers: (08)
Meinke, K., & J. V. Tucker (1993) Many-Sorted Logic and its
Applications, Wiley & Sons, New York. (09)
They use the word 'sort' as a technical term throughout that book,
but nearly every article has sentences like "Many-sorted logic
is logic for reasoning about more than one type of data." (010)
That book has several chapters on reasoning about datatypes in
programming languages, but they consistently use the word 'sort'. (011)
Then look at the article by Reynolds (1983), which is one of
the basic references for relating theoretical issues in logic
to types in programming languages: (012)
http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf (013)
He consistently uses the word 'type' in talking about datatypes in
programming languages in the same way that the above book uses 'sort'.
That word 'type' has been much more widely used for programming
language datatypes, but both words 'type' and 'sort' are widely
used in overlapping ways. See, for example, (014)
Bläsius, K. H., U. Hedstück, & C-R. Rollinger, eds. (1989) Sorts and
Types in Artificial Intelligence, LNAI 418, Springer-Verlag, Berlin. (015)
There is no consensus, even among people who have a very strong
background in logic. My recommendation is to use the word 'type'
as a generic term that includes all the uses in logic and in
programming. The special case for which Russell used the word
'type' is very rare compared to the other uses of the word. (016)
I would also like to mention another way of relating the CL
method of quantifying over relations to Russell's hierarchy of
types. Please note that all of arithmetic can be formalized
in FOL. One of the first textbooks to adopt that approach is (017)
Schoenfield, Joseph R. (1967) Mathematical Logic, Reading, MA:
Addison-Wesley. (018)
What Schoenfield does (and most authors since then) is to replace
the second-order axiom of induction with an axiom schema: a pattern
for asserting a new FOL axiom for each relation to which induction
is being applied. In effect, that provides a potentially infinite
number of axioms, but in any proof, only a finite number are used. (019)
In Common Logic, it's not necessary to introduce an axiom schema
because each statement that quantifies over relations covers all
and only those relations in the current domain. (020)
This example shows how Common Logic is able to prove theorems
that would typically require higher order logic, while preserving
a first-order style of proof. You could take any proof for
which Schoenfield (or anybody else) uses axiom schemata and
replace each axiom schema with an ordinary CL statement. The
two proofs would be line-by-line equivalent. (021)
John (022)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (023)
|