I'm not very keen on mathematical logic, but really want to study it. And as I know any try of maths foundation was using mathematical logic, so is it something that we always have as an "axiom" in maths foundations ? And do we always take the same logic for "axiom", I mean there is first-order logic, second-order logic, propositional logic (maybe I am messing up with classification, so sorry for that, I know a little about mathematical logic) ? Can be my question is not very clear, sorry for that, if it is so I will try to make it clearer. Thanks in advance.

  • $\begingroup$ I'm not entirely clear on what you're asking. You seem to be asking in your second sentence whether we include as an axiom that foundations involves logic; I would say that the word "logic" in the context of mathematics is defined to encompass foundations (as well as other things). Or maybe you're asking about whether there is some universal agreement to e.g. use specifically first-order classical logic in foundations? If that's your question, I think that's quite interesting, but it's not clear to me what you're asking. $\endgroup$ – Noah Schweber Mar 7 '18 at 18:50
  • $\begingroup$ @NoahSchweber Actually I'm asking two questions (they're related I think). 1.Is mathematical logic included in the foundations ? You said that it actually encompasses the foundations. But the reason I'm actually asking this question is that, as I know, the mathematical logic itself developes as separate section of maths, so it means when we "create" some foundations we must take the "axioms"(if I can call them in such a way) of logic as true. So it is the reason of asking this question. 2.Do we always take the same kind of logic for foundations ? $\endgroup$ – Юрій Ярош Mar 7 '18 at 20:16

Let me answer one particular interpretation of your question:

To what extent is there an agreed-upon logical framework for mathematics - and to the extent to which there is one, what distinguishes it?

(I write "what distinguishes it" deliberately: it is quite possible for something to be adopted initially for one reason, and then for other more convincing features of it to come to light later. I suspect you're less interested in the historical reasons than you are in the current analysis, although correct me if I'm wrong.)

There are several responses to this question. "One level up," there is the well-worn discussion over the role of ZFC as the "standard" axiom system within which mathematics takes place, including the following important observations:

  • Most working mathematicians cannot list the ZFC axioms.

  • As a matter of practice, the ZFC axioms are almost always much more powerful than anything we actually need.

  • That said, the ZFC axioms provide an incredibly powerful framework for analyzing principles of high consistency strength, and in light of Godel's theorem (and subsequent work, including work of Friedman) we should be interested in ways to study such principles.

  • ZFC has a reasonable claim to relative usability amongst similarly powerful systems, although that is being challenged by e.g. homotopy type theory.

  • And many others (and you can find further discussion of this topic throughout this site, including this old question).

But I think you're asking something more fundamental - about the specific logic we use to formalize mathematics in the first place. Here there are, I think, two main "axes" along which we can make decisions:

  • Expressive power. In my opinion, one of the most important "primordial" observations in mathematical logic is that propositional logic is not enough to do anything useful. While simple syllogisms are of course important, mathematics talks about objects and fundamentally uses quantification, and neither of these are things propositional logic can handle. First-order logic emerges as one candidate; the obvious alternative is second-order logic. In a precise sense, third-order logic is reducible to second-order logic, so this seems to be the main distinction. There are of course additional options, but I'd say that these two are the most important ones.

  • The nature of truth. Or, more accurately, of truth values. "Classical" logic adopts at the very beginning the idea that there are two truth values, "True" and "False," and that they interact via the logical connectives in certain specific ways - most importantly, that the law of the excluded middle holds. There are many alternatives to this, including intuitionistic logic, paraconsistent logic, many-valued logic, etc. Importantly, the "truth question" emerges even before the "expressiveness" question: it's already present in propositional logic. One possible response to this is that we should first resolve this question before moving on to the previous one; a reasonable objection is that our analysis of the structures we are trying to express facts about will inform our understanding of truth. (Incidentally, along these lines I recommend Humberstone's epic tome "The Connectives".)

Both of these inspire huge debates, which this answer box can't adequately cover. Let me say a very brief bit about the situation as I see it, beginning with my understanding of the convention which emerged:

By and large, mathematicians adopt classical first-order logic; we work inside the first-order theory ZFC, which lets us talk about higher-order concepts in a first-order way.

Or rather, this is the foundational framework which emerged around mathematical practice, and has so far proved sufficient and the norm within the foundationally-interested community.

The adoption of classical logic, I think, is most firmly ingrained: it reflects ideas about truth which the majority of the mathematical community hold. Of course this is not to say that we present a unified front here, only that it seems to be the great majority view. Note that this point is widely recognized and accepted by working mathematicians, via the common acceptance of proof by contradiction.

The adoption of first-order logic is more technical (although of course the debate around it is more narrow in audience and scope, while in my opinion no less fundamental). The main issue with first-order logic, I think, are the limits on its expressive power provided by the compactness theorem and the Lowenheim-Skolem theorem. Within logic these has come to be seen largely as positive features; in particular, compactness is necessary for us to have a good notion of "proof." Lindstrom's theorem then isolates first-order logic as a maximal logic with these properties, and this forms I think a strong basis for adopting it rather than second-order logic. Debates about the problems inherent in second-order logic can be found in many places; in particular, Quine, Shapiro, and Vaananen are good names to search for.

Finally, let me end by saying that this paper of Ferreiros may be of interest to you.

  • $\begingroup$ Your second bullet point made me chuckle and I'm inclined to disagree with it. But then again... you certainly have the majority on your side. $\endgroup$ – Stefan Mesken Mar 7 '18 at 19:21
  • 1
    $\begingroup$ @StefanMesken Fixed. :) $\endgroup$ – Noah Schweber Mar 7 '18 at 19:47
  • $\begingroup$ Thanks a lot for this big answer. This question is not related to the main but still how can we prove theorems about formal logic systems e.g. the Lindstrom's theorem ? What we use to do this ? Logic itself ? $\endgroup$ – Юрій Ярош Mar 7 '18 at 21:05
  • $\begingroup$ [+1] Very interesting. $\endgroup$ – Jean Marie Mar 7 '18 at 21:08
  • $\begingroup$ With regards to the nature of truth, my impression is that the majority on that is not the most robust thing. It doesn't seem that most mathematicians have really given it hard thought as opposed to just going with what they were told. In particular, ignorance and confusion about the alternative views seems common. I suspect I could shake the confidence of many mathematicians using fairly standard constructivist/finitist rhetoric. Admittedly, many mathematicians have thought hard about this and settled on the classical view, so I'm by no means suggesting everyone would change their minds. $\endgroup$ – Derek Elkins Mar 8 '18 at 0:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.