[FOM] Re: Michael Makkai's programme

[A.P. Hazen]

   In a recent posting (title: None), Michael Makkai has started a
description of a proposed foundational "System."  I am interested enough to
want to know more, but I fear my knowledge of category theory is below even
that low threshhold he was attempting to write for.  (The reference to a
""one-way" category of kinds" in section 3 lost  me.)
   In several places, wording in Professor Makkai's post reminded me of
ideas from elsewhere in logic and philosophy.  I don't know whether the
"echoes" I heard were intended, or whether they are more likely to help or
hinder my understanding of his project.  I would like to mention 3, for him
to comment on if he wishes.
---
   (1)  "Abstract sets." (Section 2)  The description of abstract sets
given (in part by quoting Lawvere) sounds very much like what
mathematicians uninfluenced by Frege and Russell would have found it
natural to say in the late 19th C.  (Cantor, and arguably perhaps even
Plato, seem to have IDENTIFIED cardinal numbers with "abstract" sets of the
proper cardinality!)  Kit Fine has recently tried to interpret, and make
rigorous, this older way of talking: cf. his article, 'Cantorian
Abstraction: a reconstruction and defense,' in "Journal of Philosophy" 95
(1998), pp. 599-634, and (at maybe four times the length of the article)
his book "The Limits of Abstraction" (Oxford U.P., 2002).
   --------> First question: How seriously should we take this language,
and how similar are Kit Fine's constructions to Professor Makkai's (more
category-theoretic) ones?
---

   (2)  Dependent sorts.  I think that something like the notion of
First-Order Logic with dependent sorts is very natural, and suggested by
natural English constructions (gasp!) as well as by mathematical
applications.
   Details on that claim: English and other natural languages seem to
translate more easily into MANY-SORTED than into standard F.O.L., with each
common noun translating to a new SORT of variables, so that, e.g., "Some
cat is more graceful than any dog" would be translated "EcAd(Mcd)".  But
many common nouns express relational notions.  Wouldn't it be natural to
translate, say,  "brother" by a symbol which, given a term as argument,
forms a sort of variable ranging over brothers of the denotatum of the
term?  So that, e.g., "Every man is jealous of one of his brothers" would
go to something like "Am(Eb(m)(Jmb(m)))," where "b(m)" is a variable
ranging over the brothers of m.  (Warning: some English constructions
involving "relational" nouns and generalized quantifiers seem to require
more complicated treatment.)
   ----------->Question 2: At the most basic level (say if you were trying
to explain it to mathematically unsophisticated undergraduate logic
students), is my suggested formalization of brotherhood a good example of
the logic of dependent sorts, or am I missing something essential?
---

   (3) Identity objects.  As professor Makkai describes the language of his
system, "two" objects, a and b, would be said to be identical by asserting
the existence of some object in the range of a certain dependent sort of
variable: "a=b" translates into "There exists an i(a,b)>"  This sounds a
little like an idea discussed by a number of metaphysicians, that of a
"particularlized universal" or "trope": a good introductory discussion by
John Bacon can be found on the "Stanford (Internet) Encyclopedia of
Philosophy":
    http://plato.stanford.edu/entries/tropes/
Basically, the idea is to think of a relation as a KIND of "abstract
particular," and to say that the relation holds between two objects just in
case there exists an abstract particular of the appropriate kind "between"
them.  (To use jargon suggesting the possible similarity to ideas from
constructive type theory: an abstact particular, say
Othello's-love-for-Desdemona, is an object which WITNESSES the truth of
"Othello loves Desdemona.")

   This idea is one that clearly cries out for formalization in a logic of
dependent sorts.  I think it may have many uses in different parts of
logic.  One writer who has used it in the  formulation of a theory which
may be of some mathematical interest is D.W. Mertz: cf. his 'The logic of
instance ontology,' in "Journal of Philosophical Logic" 28 (1999), pp.
81-111.  (Mertz seems to have  come to the logic of dependent sorts
independently: the convention he adopts to cover cases of variable-binding
confusion arising with such a notation is NOT the one adopted by most
writers on "polymorphic lambda calculus," or by Hailperin in his articles
in the "JSL" for 1956 (correction 1958).)
    ---------> No particular question here, since I think the use of this
idea by Mertz, or by metaphysicians like Bacon, is very different from the
use made of a similar idea in Makkai's System.  But I would be interested
if anyone with FoM interests has worked through Mertz's paper and has an
opinion on it.

---
Allen Hazen
Philosophy Department
University of Melbourne
Interests: obscure bibliography