From: Michael Makkai [makkai@prism.math.mcgill.ca]
Sent: Sunday, June 22, 2003 4:56 PM
To: fom@cs.nyu.edu
Cc: friedman@math.ohio-state.edu


A new foundation for abstract mathematics


In this and some subsequent postings, I will give a description of the program referred to in the title. I gave a talk on this at the June Chicago meeting of the ASL, and as usual, I found that I could not say half of what I had in mind, and in fact had written down on slides as well. I will try my luck in this, for me as a writer (as opposed to just a
reader) of a posting, very new medium.

This first posting will be very general in character. I will write further, increasingly technical, postings -- if there seems to be any interest, that is. 

In fact, questions concerning particular items in this and later postings are what I am looking for in the first place. Generally speaking, everything here has an easily understandable intuitive basis, which, ideally, should be grasped first in specific examples formulated in detail. For their understanding, these examples do not require any technical background, but they do require a bit of patience. I would enjoy any opportunity to explain these examples.

I use square brackets [...] to isolate parts within which I use concepts 
from Category Theory without explanation. I think, what I write can be 
read and understood  without reading the parts in brackets. There may be 
categorically minded readers who will want to see the parts in brackets. 


1. The universe and the language.

The foundational system that the program at hand is aimed at will be called simply the System. The System does not exist yet as a whole. As parts of it, there are ideas, aims and guiding principles; and then there are pieces of it that are ordinary mathematics: definitions, theorems and proofs.

The mathematics involved is invariably done in the usual framework of present-day mathematics, sometimes explicitly in axiomatic (either Godel-Bernays, or ZFC-with-Grothendieck-universes) set theory.

There are two "absolutes" involved: the universe and the language. That is, there is an uncompromising intention to conform to an ideal in each of the matters of the universe and of the language. 

The universe is intended to be comprehensive. For comparison, the Cantorian universe is, and is intended to be, comprehensive;  the "universe" of, say, second order number theory, is not, and it is not intended to be.

[As another example, the "universe" of Topos Theory (meaning doing mathematics in the framework of an elementary topos), is not comprehensive; one does category theory *over* a topos, not *in* a topos: witness indexed category theory.]

As to the language, first, the *object-*language has to be fully
explicit: it has to be  *formal*. (The metalanguage is quite optional, of
course: one is free to discuss metalinguistically the System in any way one wants to.) Secondly, and just as importantly, the language has to be 
*right*, that is, expressive: merely *coding* what we have in mind is no 
good; we have to *say* what we mean. I would like to refer to what was 
said in this paragraph as *Frege's imperative". 

[Topos theory is not, in the first place, a formal theory, although there exist formal approaches to it.]


2. Totalities as types.

The 19th century witnessed the discovery of abstract totalities and their capacity to represent mathematical objects ("naive set theory"). The concept of totality as *type*, albeit not necessarily coached in that term, appeared early. I regard the System to be, in the first place, an elaboration of "naive type theory".

Comparisons of the System with (non-naive) type-theory proper will be made 
in the sequel. 

The basic characteristics of type theory is the acceptance of the presence of fundamentally different kinds of the entities, whose relations to each other are mediated by a substantial additional equipment. The language of type-theory is burdened with "type-discipline": an ever-present need to acknowledge the specific types of entities the discourse is about. Type theory gives up the hope that the world can be explained as consisting of elements ultimately of the same nature. It resigns itself in the irreducible variety of the world, and tries to find solace in the unfolding panorama of this variety.

One may say that type theory is a "physical theory" of the abstract:  
"physical" in that it accepts abstract entities as given in and by the world, rather than generated by idealized mental acts. In contrast, the conception of totality as *class*: as the result of *comprehending* entities that answer a description (have a property) into a totality, would have place in a "conceptual", "non-physical", attitude.

Andreas Blass just posted (Thu, 19 June 2003; "[FOM] real numbers") a nice 
description of the (ideal) mathematician's "type-theoretic" view of the 
world of mathematics. 

I think, in one way or another, all of us are still in the shock from the crash, exemplified by the Russell paradox, of the unbridled conceptual attitude. Type theory is shock management: it is an inherently cautious, piecemeal approach. It does have its satisfactions though.


2. Abstract sets

For a very good introduction to "abstract sets", I recommend section 2 of F.  W. Lawvere's paper "Variable Quantities and Variable Structures in Topoi" (in: Algebra, Topology and Category Theory (A. Heller and M.  
Tierney editors), Academic Press 1976, pp. 101-131; quoted below as [L]). Section 2 is on pages 118-128, and can be read quite independently from what comes before in the paper.

Abstract sets are well-known to logicians: they are sets consisting of
*urelements* (atoms, points) alone. I think, this notion of "set" is the "original" idea of set. (It is something distinct from the concept of
"class": see above. Modern set theory fuses the original concepts of "set" and "class", to separate them again at a new dividing line.)

Jon Barwise, in his book "Admissible Sets and Structures" (Perspective in Mathematical Logic ("Omega-series"), Springer, 1975), argues for the use of urelements (Chapter 1, section 1, pages 7 to 9). He starts out by
saying:  

" ... we allow (admissible) sets to contain urelements. Bluntly put, we consider (admissible) sets which are built up out of the stuff of mathematics, not just the sets built up from the empty set." 

(The parentheses around the two occurrences of "admissible" are my own
addition.) 

I will now take a more radical point of view: I'll admit *only* urelements as elements of sets; in other words, "set" from now means "abstract set".  

In explicating the concept of (abstract) set, I follow Lawvere who says [L; p.119]: 

"An abstract set X has elements each of which has no internal structure whatsoever;  X has no internal structure except for equality and inequality of pairs of elements, and has no external structure save its cardinality; still an abstract set is more refined (less abstract) than 
a cardinal number in that it does have elements while a cardinal number 
does not".

We are at a decisive juncture: we have to answer "Frege's imperative" (see 
above). In fact, the best way of explicating the idea of "abstract set" is 
to place it into a (potentially) formalized language.


3. First Order Logic with Dependent Sorts (FOLDS). 

(See also my paper "Towards a Categorical Foundation of Mathematics", in:  
Logic Colloquium '95 (J. A. Makowsky and E. V. Ravve, editors), Springer Lecture Notes in Logic, no. 11, 1998, pp. 153-190; and the (unpublished) 
monograph called FOLDS at: www.math.mcgill.ca/makkai/. 

FOLDS is used in a large variety of contexts going beyond (abstract)  
sets in System; I will turn to these contexts later. First, a general description, followed by examples of uses for talking about sets (and later functions).

FOLDS is a constrained form of ordinary First Order Logic (FOL). In FOLDS, variables are typed (or sorted, if you wish); types (sorts) may be dependent on variables. There is a mutually recursive character to the declaration of variables and the formation of types. To start the recursion, there must be types that depend on no variable. Each type, dependent or not, is headed by (in case it is not dependent, just is) a 
"kind". 

(Dependent types are well-known in logic; see e.g. P. Martin-Lof: An Intuitinist Theory of Types. Proc. Bristol Logic Coll., North-Holland,
1973.)

Just as in model theory for talking about a definite species of structure, or for stating the extralogical primitives of a formal system, we fix a *signature*. It is an important, and somewhat unexpected, fact that the discipline of variable-declaration and type-formation associated with a given FOLDS signature is entirely specified by a very simple kind of
structure:  a category, in fact of a special kind of ("one-way") category, whose objects are the kinds. The arrows of the signature category and their composition structure are used to define the meaningful ways of declaring variables and forming types.

In FOLDS, there is no equality as a logical primitive. In fact, there are no relations or operations as (extralogical) primitives at all. Relations are expressed by using dependent types, and operations are avoided altogether.  The formation of formulas starts with the propositional primitive (nullary propositional connective) TRUE.

It should be emphasized that, despite its constrained nature, FOLDS is an "all-purpose" language, just like FOL. In particular, we may adopt any signature of the general kind mentioned above. Indeed, in elaborating the full system, we make extensive use of whole families of FOLDS signatures.  
Also, FOL, or even multi-sorted FOL, may be regarded as a bottom level special case of FOLDS, in which there are only two levels of types: ones that are not dependent, and ones that are dependent on variables of types of the first kind.

Here is an example of a sentence in FOLDS, talking about sets and 
"equality". We have "equality" only for elements already declared to be 
elements of the same set.

First, abbreviate:  

	x=y  ::=::  (there-is e in Eq(A,x,y)).TRUE

The sentence, expressing the symmetry of equality on any set  A :

(for-all A in Set)(for-all x in El(A))(for-all y in El(A))(x=y <--> y=x)

The signature involved in this sentence has the kinds Set, El, and Eq.  
In the signature category at hand, we have the generating arrows (I'll call them "grammatical arrows")  el:El--->Set and eq_0:Eq--->El, eq_1:Eq--->El; the two composite arrows Eq--->Set are declared to be equal (we have defined a very small category of three objects and four non-identity arrows via generators and relations). For now, I leave it to the Reader to puzzle out, using this example and the next one in the next section, how the structure of a signature category dictates the grammar of variables and types.


4. Functions and categories

So far, there has been no way of relating of elements of two different sets. We extend the above language of sets with a new primitive, "function", to provide a "variable" way of relating elements of two different sets. The grammar of "function" uses the additional kinds Ar (for Arrow) Ap (for Application) (with further two grammatical arrows
Ar--->Set, one of the form Ap--->Ar , and two Ap--->El).  Here is the
way these kinds are used, shown as a system of variable declarations (without making any statement about the variables involved):

	(A in Set)(B in Set)(a in El(A))(b in El(B))(f in Ar(A,B)) 
	(t in Ap(A,B,a,b,f))

Of course, in our last move, we partly followed the example of Category 
Theory -- I say "partly" because Application is not category theoretical. 
In fact, the use of Application can be replaced by the categorical kind Composition, leading to a system that avoids talking about "elements" 
altogether.


I stop now, with a promise to continue. I am ready to listen to advice how 
to, and/or how not to, proceed.