10

After posting this question (in particular after Carl's and Peter's answers) I have realized that the answer seems to depend on a basic problem in foundations.

Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets. These are treated at an intuitive level. Using set theory they define languages, axioms, theories, models and all the logic toolbox. Then they define (formalized) set theory again, using this language.

The second point of view is typical of logicians. They realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead. Then set theory is formalized in this framework.

I always thought that the points of view were interchangeable, as far as one was interested in the mathematical consequences. But comparing Carl's and Peter's answers it seems that actual (but still foundational) mathematic may depend on the point of view accepted. I'd like to understand this better.

Are there any mathematical consequences of choosing one of the two points of view?

Community
  • 1
Andrea Ferretti
  • 14,454
  • 13
  • 78
  • 111
  • 4
    I don't think your perception of logicians is correct. It would be fun to have a poll, but I can only think of a few logicians whose point of view is close to your 'second point of view.' – François G. Dorais Apr 29 '10 at 20:36
  • 3
    In fact, this seems more true of mathematicians than logicians, strangely enough. You might say that the second viewpoint is very much the perspective of Bourbaki. – Harry Gindi Apr 29 '10 at 20:52
  • 2
    Your description of logicians is thoroughly mistaken. – Andrej Bauer Feb 09 '13 at 08:31

2 Answers2

9

I would like to question two statements you make because they paint an oversimplified picture, which unfortunately is alluring to mathematicians who do not want to think about foundations (and they should not be blamed for it anymore than I should be blamed for not wanting to think about PDEs).

  • "Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets." This is what mathematicians say, but most cannot even tell you what ZFC is. Mathematicians work at a more intuitive and informal manner. High party officials once declared that ZFC was being used by everyone, so it has become the party line. But if you read a random text of mathematics, it will be equally easy to interpret it in other kinds of foundations, such as type theory, bounded Zermelo set theory, etc. They do not use the language of ZFC. The language of ZFC is completely unusable for the working mathematician, as it only has a single relation symbol $\in$. As soon as you allow in abbreviations, your exposition becomes expressible more naturally in other formal systems that actually handle abbreviations formally. Informal mathematics is informal, and thankfully, it does not require any foundation to function, just like people do not need an ideology to think. If you doubt that, you have to doubt all mathematics that happened before late 19th century.

  • "They [logicians] realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead." I do not know of any logicians, and I know many, who would say that logic is "God-given", or anything like that. I do not think logicians are born into a life rich with the "full power of set theory" which they throw away in order to become ascetic first-order logicians. That is a nice philosophical story detached from reality. The logicians I know are usually quite careful, skeptical, and inquisitive about foundational issues, reflect carefully on their own experiences, and almost never give you a straight answer when you ask "where does logic come from?" Your view is naive and inaccurate, if not slightly demeaning.

If I understand your question correctly, you are asking whether there is a difference between the following two views:

  1. We start with naive set theory and on top of it we formalize set theory.

  2. We start with first-order logic and immediately formalize set theory.

Well, we are proceeding from two different meta-theories. The first one allows us a wide spectrum of semantic methods. We can refer to "the standard model of Peano arithmetic" because we "believe in natural numbers", and we can invent Tarskian model theory without worrying where it came from.

The second method is more restricted. It will lead to syntactic and proof-theoretic methods, since the only thing we have given ourselves initially are syntactic in nature, namely first-order theories. There will be careful analysis of syntax. For advanced methods, however, we will typically resort to at least some amount of "naive mathematics". Ordinals will come into play, it will be hard to live without completeness theorems (which involve semantics), etc.

However, this is not how real life works. The dilemma you present is not really there. A working mathematician does not concern himself with these issues, anyhow, while a logician will likely refuse to be categorized as one or the other breed.

That is my guess, based on the experience that my fellow logicians are complicated animals and it is hard to get to the bottom of their foundational guts.

Andrej Bauer
  • 47,834
  • 5
    Many professional mathematicians have this question about the egg and the chicken in one way or other. Most don't even bother or dare to ask. I think it is good that some of them at least ask.

    One can tell them that they are "thoroughly mistaken" are spreading "fairy tyles" and are "demeaning" towards logicians. One can also think: "Hm, if so many of my otherwise esteemed are so confused about what my community understands so well, then maybe we missed to write the good exposition of this fact that everyone would read!" Something like an AMS-notices 'What is... foundations?'

     – Urs Schreiber Feb 09 '13 at 15:16
  • Good point, so the question is badly asked and badly answered. It is a bit of news to me that "our community" understands the issue so well. Do we? You should definitely write your our answer to the question (and first explain how you understand the question). – Andrej Bauer Feb 09 '13 at 15:31
  • What is this question of "chicken and the egg"? – Andrej Bauer Feb 09 '13 at 15:35
  • 2
    The "Chicken and egg"-question about mathematics:

    Does mathematics root in a formal foundation or is there an infinite recursion (the "turtles" in Peter's answer referred to above.) of foundational systems or else just an "intuitive notion of sets" at the beginning? (If the latter, what if our inutiotions differ?) In either case: where, if at all, does it matter for actual mathematical results on which level one roots one's mathematics? (This last one is concretely the question of this thread, I think).

    Peter's answer referred to above starts answering these things, I'd say.

     – Urs Schreiber Feb 09 '13 at 17:16
  • Ok, I totally missed that in the question. I should have read it more carefully. Thanks for explaining. @Andrea, is that what you asked? – Andrej Bauer Feb 09 '13 at 18:14
  • It may be a little late to say this now, but yes, this is what I had asked :-) – Andrea Ferretti May 23 '19 at 16:18
  • It's never too late for me to write even more embarrasing things on the internet, to be remembered by Google forever. I will put in an addendum (and be more polite). – Andrej Bauer May 23 '19 at 20:45
  • I have now wasted an hour trying to say something sensible and short, and failed. If I can think of anything to say, I'll post it here. – Andrej Bauer May 23 '19 at 21:53
5

Well, here's what it seems like: We had the naïve set theories of Cantor (unaxiomatized) and Frege (first axiomatization), and everything was right with the world. Then, however, it eventually became clear that there were paradoxes that made the theory inconsistent, so Zermelo and Russell (and others) both set to work on coming up with alternative axiomatizations to deal with the paradoxes. Russell's Theory of Unramified Types ended up being unusable (cf. the proof that 1+1=2 in Principia Mathematica (the full proof is something like 100 pages). However, Zermelo was able to recover a good deal of naïve set theory in the Z (ZC), or Zermelo (resp. Zermelo + Choice) axiomatization (Zermelo+Choice).

However, it eventually became clear that Z(C) was too weak in some regards, so Fraenkel and Skolem both proposed (independently) the axiom schema of replacement to improve the power of the theory. If you include the axiom schema of regularity (which says that $\in$ is well-founded), you get ZF (resp. ZFC).

Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets. These are treated at an intuitive level. Using set theory they define languages, axioms, theories, models and all the logic toolbox. Then they define (formalized) set theory again, using this language.

ZFC is built on first-order logic. Mathematicians then can construct models of languages and set theories internal to ZFC. (To answer your comment: The reason why we want to axiomatize over first order logic is because first order logic has all of the properties one would want from it, completeness, compactness, etc. In particular, the reason why we must first define theorems and proofs is because we need a proof calculus to be able to formally derive results.)

The second point of view is typical of logicians. They realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead. Then set theory is formalized in this framework.

In fact, this is true for both mathematicians and logicians (although this view is strangely more popular among mathematicians than logicians). This would be the "bootstrapping" step for mathematicians to get to ZFC. Even though Bourbaki's book on set theory has an inadequate and confusing approach to set theory, the idea in the first few sections is correct. One first defines a what it means for something to be a theorem, what it means for something to be a proof, etc, then gives the axioms of formal logic, then constructs a set theory above that (this was one of the areas in which Bourbaki was the most influential as well. That is, his opinion on the logical grounding of set theory (but then not actually worrying about it once it's developed) is perhaps one of his most important lasting contributions to the world of mathematics.

Harry Gindi
  • 19,374
  • It seems you are implying that no mathematician holds the first point of view. I'm afraid I am a counterexample. My point of view (and of most people I heard) is that one can surely talk about sets without defining proof or theories first. Just give the axioms (in the layman, not formal sense) and derive the usual informal set theory. Then define logic as any other branch of mathematics. And if you wish you can then do set theory again in this framework. – Andrea Ferretti Apr 29 '10 at 22:50
  • 3
    Just a small historical correction. Cantor did not propose a formal theory in any reasonable sense of 'formal'. Frege was the first to recognize the need for a formal theory of sets. In fact, it's apparent that Cantor did not believe that any of the paradoxes were refutations of his ideas. Indeed, he discovered a paradox a few years before Russell and that did not seem to bother him much. It's unclear (to me) whether Cantor ever felt the need for a formal theory of sets. – François G. Dorais Apr 29 '10 at 23:13
  • Yes, that was implied. I was thinking of just including Frege, but if I'm talking about the history, I can't just not mention Cantor. – Harry Gindi Apr 29 '10 at 23:37
  • 1
    I also would like to register as someone holding the first point of view. As an undergrad, I had imagined that logicians would somehow build up set theory from the beginning, and never use any tools like functions, natural numbers, or sequences until they had been defined internally. Then I took a course in logic, and found that functions, sequences, etc., showed up in droves long before they were defined. I was confused for a bit, and then went back to my way of approaching other math, assuming that these symbols, languages, etc. were really sets described by some background set theory. – Charles Staats Apr 30 '10 at 01:26
  • @Charles: If you're interested in reading a completely formal exposition of set theory from nothing, Bourbaki does this in chapter I of Théorie des Ensembles. My statement about how their set theory is inadequate is mainly about chapter II (It does not contain the axiom of replacement, according to François and Joel, who have linked to a paper in the past (although I can't remember who wrote it)). Everything is defined in terms of (essentially) formal symbols. It's useless and totally impractical, but it's definitely worth looking over. – Harry Gindi Apr 30 '10 at 01:36
  • 1
    @Andrea: If you do that, then you are not being strictly formal. The rules of inference from logic are necessary to prove anything from the axioms of set theory. I don't believe that there is any way to avoid circularity just defining the axioms of set theory (unless one includes the axioms of logic as well). – Harry Gindi Apr 30 '10 at 02:17
  • Of course there will be circularity whatever foundation you choose. My point of view is that I do not need axioms of logic to carry out a reasoning. I can deduce theorems about sets from their axioms much in the way you do usual mathematics. To be more clear: I do not need rules of logic because I do not do carry out any formal deduction, meaning manipulation of symbols. This because I take axioms of set theory as they are stated in natural language. – Andrea Ferretti Apr 30 '10 at 10:21
  • 2
    The whole point of doing it formally is to avoid circularity. You can actually do it. – Harry Gindi Apr 30 '10 at 11:35
  • I think we are actually misunderstanding each other, but sadly I do not have time to elaborate now. By the way, is it really convenient to have such a long discussion in the comments? – Andrea Ferretti Apr 30 '10 at 12:04
  • You have my e-mail address if you'd like to continue this conversation there. =) – Harry Gindi Apr 30 '10 at 12:17
  • Your first paragraph is a fairytale, not history. – Andrej Bauer Feb 09 '13 at 08:33