# Set theory and alternative foundations

Every foundational system for mathematics I have ever read about has been a set theory, from ETCS to ZFC to NF. Are there any proposals for a foundational system which is not, in any sense, a set theory? Is there any alternative foundation which is not a set-theory?

-
Question too vague (at present) to admit a proper answer. You haven't said what you mean by "not a set-theory"; nor does what you have written give any idea what an "answer" to your question would involve. – Yemon Choi Dec 3 '09 at 1:18
I've no idea what "some kind of discontinuity instead of object/set" is supposed to mean. Set theory was simply found to be an extremely useful foundation for much of modern mathematics (and that's to put it mildly). Why do you want another foundation? Why do you suggest that it most possess some different ontological assumption, whatever that means? Please note that this isn't a good place to have a discussion - if you're unable to frame a concrete mathematical question, that's fine, but you may have better success at other forums. – Alon Amit Dec 3 '09 at 1:24
The short answer to "are there any alternative foundations exist" is no, not really. Set theory itself has a couple of different formalisms, but I don't know of anything else that was found to be useful as a foundation. – Alon Amit Dec 3 '09 at 1:39
Bill Lawvere has suggested axiomatizing the category of categories as a foundation of mathematics, and there is no sense in which this could be thought of as a set theory. Colin McLarty is one person who has done some work on achieving such an axiomatization. – Steven Gubkin Dec 3 '09 at 11:17
This seems like a real question to me. It is of interest to me, but maybe it is Philosopher Steve, not Mathematician Steve who is interested. Obviously the question could be better posed. This would be my post (if I were psihodelia) "Every foundational system for mathematics I have ever read about has been a set theory, from ETCS to ZFC to NF. Are there any proposals for a foundational system which is not, in any sense, a set theory?" – Steven Gubkin Dec 3 '09 at 19:55

Bill Lawvere has suggested axiomatizing the category of categories as a foundation of mathematics, and there is no sense in which this could be thought of as a set theory. Colin McLarty is one person who has done some work on achieving such an axiomatization.

-
Somebody now seems to have asked/answered a question describing this in detail: mathoverflow.net/questions/8731/… – Ilya Grigoriev Dec 13 '09 at 8:53

If we adopt a historical attitude, then there is an extremely good answer, namely, Geometry. For approximately two thousand years, (Euclidean) geometry was taken to be the foundation of all mathematics. Numbers were regarded as lengths of line segments; quadratic equations were regarded as expressing the relationship of the areas of certain geometrical figures. All mathematics was, at bottom, geometric.

Of course, there were problems with this. For many ancient mathematicians, for example, it made as little sense to add the cube of a number to its square as it would to add a volume to an area. The equals sign was not introduced until 1557, and it is easy for contemporary mathematicians to lose sight of how differently the ancients thought about the mathematical objects they studied and wrote about. Newton, famously, was so great a mathematician that he was able to introduce the differential calculus in terms of the ancient geometrical reasoning, although we rarely conceive of his ideas that way today. Indeed, much of this kind of writing now appears alien to us.

-
Unfortunately Geometry, at least in the form axiomatised by Tarski (see en.wikipedia.org/wiki/Tarski%27s_axioms), lacks the expressive power needed to be a good foundation for other branches of mathematics. – Dan Piponi Jan 18 '10 at 21:00
Has there been recent work that uses geometry as a foundation of mathematics? I'm very interested in pursue this further. – user2529 May 16 '10 at 9:34
It may be too naive to formulate addition as concatenation of lengths/areas/volumes. Take something geometrically simple like translation for instance. It took till 1500 Descartes for this to be formulated properly in terms of coordinates (and vector spaces). It involves not just the idea of translation as addition or subtraction, but also the idea of triples of numbers to represent space. We must not rule out the possibility of geometry being able to formulate addition, not directly, not via layers and layers of symbolization, representation and ideas. – user2529 May 16 '10 at 9:42
@Colin: Using Desargues' Theorem one can define basic arithmetic operations (on the points of a line) geometrically. So one can use geometry as a foundation for some portions of arithmetic. As sigfpe notes, however, it seems that (synthetic) geometry alone is not powerful enough to be a foundation for all of mathematics unless you sneak in some set theory through the back door. – Timothy Chow May 17 '10 at 14:35
Perhaps synthetic geometry needs a more powerful axiomatization, sigfpe and Timothy? – user2529 May 22 '10 at 10:46

Type theories form another class of foundations for mathematics, and are used in various places. For example, Martin-Löf type theory is a constructive foundation of mathematics, and a lot of constructive mathematics has been formulated in it.

Type theories are used in some proof assistants, like Coq, and they have nice connections with various programming languages in computer science - look up languages with dependent types.

I should also mention that type theories have a close relation with categories - "Introduction to higher order categorical logic" by Lambek and Scott connects various type theories and categories.

-
For a study comparing all three approaches see Steve Awodey's From sets, to types, to categories, to sets andrew.cmu.edu/user/awodey/preprints/stcsFinal.pdf – Steven Gubkin Dec 4 '09 at 21:55
To me it is questionable whether type theories are really different from set theories, or whether they merely lie at opposite ends of a continuum. To be sure, it would be hard to recast ZFC as a type theory in the traditional sense, or System F as a set theory in the traditional sense, but there is considerable overlap in the middle. It's hard to distinguish ETCS, for instance, from the higher-order type theory that is the internal logic of a topos. – Mike Shulman Dec 5 '09 at 21:36

Arithmetic can be used as a foundation for a surprising amount of mathematics. The book Subsystems of Second-Order Arithmetic by Steve Simpson demonstrates that a huge fraction of mathematics can be formalized arithmetically. In fact, first-order Peano arithmetic suffices for most "ordinary" mathematics.

I should point out, however, that even when using arithmetic axioms as one's ultimate foundation, people in practice formalize everything in (finitary) set theory first, and then show how to encode finite sets as integers. Set theory is just so darn convenient as a unifying language that it's hard to get away from it entirely. However, as long as you're really only dealing with finite or countable sets, almost anything you want to state and prove can in principle be done with integers, so in this sense arithmetic can be used as a foundation for most of mathematics.

Areas of mathematics that are "intrinsically uncountable" cannot be captured by any of the systems in Simpson's book, but there are fewer of these areas than you might think.

-

This was going to be a comment to Joel David Hamkins's answer on geometry, but it didn't fit.

+1 This is one of the most clear-minded things I have read on MO. It does not make a mockery of Foundations and still says something non-obvious.

I'm very skeptical of all this business with category theory being a foundation for mathematics. First, whenever anyone talks about it, it always seems to be somebody else's work. It's become something of a meme that "Bill Lawvere has proposals to provide foundations for math through category theory", but we don't ever see details provided.

Second, are we really to understand that we are going to add small integers with arrows and diagrams? Draw circles and lines, and say that the latter meet at most once? I think people work in trans-Euclidean hyperschemes of infinite type so much, they forget that math includes these things.

As Wittgenstein remarks in the Investigations, just because you can express A in terms of B, it does not mean that B actually underlies A.

-
"Second, are we really to understand that we are going to add small integers with arrows and diagrams?" Think of the analogue for set theory: are we really to understand that a real number or a triangle is a set of sets of sets of sets ... of sets? – Omar Antolín-Camarena Mar 19 '11 at 1:35
Regarding "all this business with category theory being a foundation", I'm not sure what your true grounds for skepticism are -- have you ever tried investigating this? If you asked a question on MO (phrased in suitably non-subjective, non-argumentative language, of course), you might get a thoughtful reply. One recent development pertaining to foundations and which connects homotopy theory, intensional type theory, and higher category theory, has been discussed recently at the n-Category Cafe. See especially the posts Homotopy Type Theory I and II. – Todd Trimble Mar 22 '11 at 22:19

I believe the lambda calculus was originally intended as a foundation for mathematics. More recently it seems that both category theory and type theory seem to be gaining support. Although, I think type theory (a la Martil-Löf) could be viewed as another variation on the set-theoretic theme.

-
Nice thread resurrection. =\ – Harry Gindi Jan 18 '10 at 17:54

Von Neumann wrote down a foundation where the basic objects are functions, not sets. But it was soon re-cast into an equivalent system with sets (and classes).

-
Hey! I know you! Your my Analysis recitation instructor! – Steven Gubkin Dec 5 '09 at 0:24
@Gerald Lawvere and Rosebaugh do something very similar in "Sets for Mathematics",using functions as the elements of thier foundations.But they don't eliminate set theory either-they use the functions to build sets rather then the converse. Sets have the enormously important advantage of complete determinacy of thier composition and it's not entirely clear that a foundation for mathematics devoid of them would preserve this property. I think this would be very problematic for most classical mathematics. – The Mathemagician Jun 9 '10 at 16:41

To follow up further on Joel David Hamkins's answer on geometry, Frege’s last work (two despairing decades after Russell’s Paradox demolished his Grundgesetze der Arithmetik) was a brief unpublished paper entitled “Neuer Versuch der Grundlegun der Arithmetik,” based on geometry with “the final goal, the general complex numbers.” (As in the Grundgesetze, he emphasizes that real numbers are ratios of quantities, not quantities themselves.)

-

This may not satisfy the request for something that is "not, in any sense, a set theory" but Oliver Deiser has worked out two versions of foundations, one based on lists and one on multisets. This is in his book "Orte, Listen, Aggregate" (and his Habilitationsschrift with the same title).

-
@Andreas Blass Thank You. Especially interested in lists (for computers lists are the basic, sets come afterwards: sets are equivalence classes of lists, or categorically, one 'forgets" from LIST into SET) I went to his web page, but could not find a downloadable summary of his foundational research. There seem to be a published book, which I may buy if nothing else is available for free. Any pointers? PS Werke auf deutsch wurden auch gut sein) – Mirco A. Mannucci Jun 2 '11 at 22:56
@Mirco Mannucci: I've just e-mailed a copy of Oliver Deiser's Habilitationsschrift to you (or to someone with the same name as yours --- I got your e-mail address from Google because it's not in your MO profile). You might also be interested in a paper "Why Sets" that Yuri Gurevich and I wrote a few years ago. It's available at math.lsa.umich.edu/~ablass/set.pdf (and also at Yuri's web site at Microsoft). – Andreas Blass Jun 3 '11 at 0:04
Correction: The right source for "Why Sets" is Yuri Gurevich's page, research.microsoft.com/en-us/um/people/gurevich/Opera/172.pdf because the version on my web page is an older one (written before Deiser's work). (One of these days, I'll update my web page.) – Andreas Blass Jun 3 '11 at 0:11

I know from the logical end there is plural quantification developed and expounded to some extent by Boolos, Lewis and others that sidesteps the whole issue of set and gives first order logic the ability to talk about set-like objects without resorting to set theory.

-