[FOM] None

[Michael Makkai]

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.