Sorry if this is off-topic.

It was my attempt to take a top-down approach to mathematics.

Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as a foundational system. However, other set theories exist (e.g. NBG), the axiom of choice is famously "controversial", and then there's other approaches entirely, like type theory (e.g. HoTT) and category theory.

Alright, but these seem to have some structure in common... enter universal logic, for which I found Meseguer's paper particularly enlightening. For a brief moment I thought I had reached my goal (despite the fact that the theory about logics was itself already quite mathematically sophisticated).

But then I discovered that, to describe different logics, one needs (or desires?) a logical framework to operate in. Pfenning's paper gives a lovely introduction to this topic, but also mentions that there are a multitude of logical frameworks, e.g. ELF or Martin-Löf's Framework, so I'm still not where I want to be.

Then, finally, I came across a paper entitled "A Framework for Defining Logical Frameworks". At this point I thought to myself that perhaps my approach thus far is misguided, given that the more effort I make, the less clear things seem to become.

And hence, my question: Where does it all begin?

Or, should this be unanswerable, is there some sort of guide through this flurry of terminology and meta-metamathematical research? It seems authors have such a clear grasp on the confines of each topic, yet somehow I cannot satisfy my simple desire to find a point at which to start. What would Bourbaki do, if they were to start writing today instead of 80-something years ago?

  • 7
    $\begingroup$ This is an interesting line of thought, but in my opinion not appropriate for this forum. I think the answer will be a personal viewpoint arising from years of reading and deep thinking. Keep it up, and have fun! $\endgroup$ Mar 19, 2021 at 6:17
  • 3
    $\begingroup$ My personal, current opinion: Formalization of mathematics begins with finite strings of symbols. Mathematics itself is a process of the mind, and the mind is not a finished product, so there is no beginning. $\endgroup$ Mar 19, 2021 at 7:46
  • 3
    $\begingroup$ A thing to keep in mind is that the logical hierarchy of topics is rarely the same as the order they should be studied in. Furthermore you are allowed to obtain basic knowledge in one topic, move on to something else and then come back at a later time. This is true even if you take Bourbaki as a guide (which I wouldn't recommend). Their books weren't written in order. They started with only a short summary of set theory without proofs, then got all the way to integration, before finally writing the proper volume on sets 15 years after the initial summary. $\endgroup$
    – mlk
    Mar 19, 2021 at 8:23
  • 36
    $\begingroup$ While I understand the impulse to sort out foundational issues before you start learning "real" mathematics, I think it is misguided. All the programs you'll find for setting up the foundations came in response to issues that arose in mathematical practice, and it is impossible to understand them without having the mathematical maturity/experience to appreciate those issues. Almost all mathematicians work in basically a naive version of ZFC (of the sort that you can read about in Halmos's "Naive Set Theory"), and I think that trying to do more than that at the beginning just won't work. $\endgroup$
    – Irina
    Mar 19, 2021 at 15:56
  • 3
    $\begingroup$ I don't think that there is a single beginning. Math, or what we now call math, requires a foundation, but there are several possible foundations, and to a large extent mathematics is independent of the foundations. Now, whatever your choice of foundation, you have to be able to do certain basic things, like induction and counting arguments. So maybe those basic ideas are the beginning and foundations are a framework built around those ideas. $\endgroup$ Mar 20, 2021 at 0:52

3 Answers 3


One approach, mentioned by Pace Nielsen in the comments, is to start with what I call strict formalism. The only substantive assumption required for strict formalism is that you are capable of recognizing and manipulating finite strings of symbols in certain simple ways, and can understand what a syntactic rule is at the level of being able to confirm or disconfirm whether a particular syntactic rule is being obeyed. So for example, it is assumed that you do not balk at assertions such as, "$\phi$ is the same symbol as $\varphi$" or "appending the symbol 0 to the symbol 1 yields the string 10". If you are bothered by the concept of a symbol, or of a syntactic rule, then I don't think that you will be able to develop anything remotely resembling mathematics.

In strict formalism, the symbols do not mean anything. It is assumed that you have the capability of verifying that if you start with certain strings and apply certain rules then you will arrive at a certain result. But there is no assumption that you are able to reason mathematically. For example, consider the rule "append a 0" and consider applying that rule some finite number of times to the string "0". As a strict formalist, you will be able to confirm that at some point, the string 0000 will emerge. However, consider the following claim: "At no point will this process ever produce a string with the symbol 1 in it." While this claim may seem ridiculously obvious, it is not a claim that a strict formalist can deduce. Arriving at such a conclusion requires reasoning about symbols, and a strict formalist is assumed only to be able to carry out symbolic manipulations, not to be able to reason about them.

A strict formalist can verify any formal proof produced by a mathematician, and so in that sense can reproduce all the formal content of mathematics, no matter how arcane an axiom is invoked. But a strict formalist will not, for example, be able to tell us something like this: "If you write a computer program to search for strictly positive integers $a$ and $b$ such that $a^2 = 2b^2$, then the program will never halt." The strict formalist will be able to execute such a computer program, and can even verify a formal proof that $\sqrt{2}$ is irrational, but as far as the strict formalist is concerned, the formal proof that $\sqrt{2}$ is irrational is simply a meaningless sequence of symbolic manipulations, and tells us nothing about "reality."

If you want to recover the ability to claim with confidence that computer programs that search for positive integer solutions to $a^2 = 2b^2$ are doomed to fail, then you need to take an additional step beyond strict formalism. Namely, you need to claim that there is such a thing as sound mathematical reasoning, and you need to lay down the principles that you think are trustworthy. At this point, it's basically up to you to decide what principles you trust. Most mathematicians seem to be happy with ZFC, but others are uneasy with it and prefer to back off to some set of more modest principles. For almost every mathematician $M$, it is possible to write down a set of formal axioms with the property that anything the strict formalist deduces from those axioms will be accepted by $M$ as a true mathematical statement. So again, in that sense, the strict formalist can reproduce all of mathematics. But the set of formal axioms accepted by $M$ will vary as $M$ varies.

  • 1
    $\begingroup$ Related to this is the Mathematics StackExchange question/answers Foundation of Formal Logic, especially (in my answer) the excerpt of Martin Davis' 1959 review in Scripta Mathematica of Church's book Introduction to Mathematical Logic. $\endgroup$ Mar 19, 2021 at 17:22
  • 3
    $\begingroup$ @DaveLRenfro Interesting MSE question. In the first edition of Kenneth Kunen's book Set Theory, on page 39, he raises the question, "But what is a symbol?" He sidesteps this question by defining symbols in terms of natural numbers. Of course that presupposes that one understands what a natural number is. Evidently, in those days, the concept of a natural number was considered clearer than the concept of a symbol. Nowadays, my anecdotal experience is that it is the other way around. I believe that in the 2nd edition of his book, Kunen no longer defines symbols in terms of natural numbers. $\endgroup$ Mar 19, 2021 at 17:41
  • 5
    $\begingroup$ +1: thank you for an enormously illuminating and interesting answer $\endgroup$
    – user147820
    Mar 19, 2021 at 21:57
  • 2
    $\begingroup$ "Strict formalist" - oh so that's the name of what I am. I think... $\endgroup$
    – Qfwfq
    Mar 20, 2021 at 0:16
  • 2
    $\begingroup$ @Qfwfq So you're agnostic about whether applying the rule "append a 0" finitely many times to the strong "0" will ever result in a string containing a "1"? $\endgroup$ Mar 22, 2021 at 0:47

Here is a possible viewpoint to contemplate:

Foundations of mathematics do not begin anywhere.

This happens to be my (current) personal belief. I agree with Monroe that the answer to the question asked can only be a personal viewpoint that is formed after some amount of experience and contemplation.

To elaborate a little bit, let me say that of course foundations and logic are tremendously useful for mathematics, and they help clarify and make precise the very nature of mathematical thinking, but the idea that they "come before mathematics" or that they "provide an unshakable foundation upon which mathematics stands" is misguided, because it is just a Creation Myth dressed up as science.

A typical foundation of mathematics builds things up in some way, for example:

  1. Syntax
  2. Formal system
  3. Logic
  4. Set theory

Type theory operates in much the same way, except that the last two steps are different. This order of steps is the result of an engineering design, which we should hope is a good one, but it seems all too easy to assign too much philopshical significance to it.

I suppose my point is to be aware of unconscious assumptions that permeate discussions about foundations, in this case an (unwarranted) desire to find the First Cause.

  • 16
    $\begingroup$ I agree. In my experience, one of the biggest stumbling blocks people have (and I mean not just undergraduates but also professional mathematicians) when they approach the study of logic and set theory is a tacit expectation that they have to suspend all their mathematical beliefs in order to avoid "circularity." A proof that they would unhesitatingly accept when it comes out of the mouth of, say, a number theorist is suddenly rejected when it comes out of the mouth of a logician. I have to explain that formal logic can clarify mathematical reasoning but cannot justify it ex nihilo. $\endgroup$ Mar 20, 2021 at 12:56
  • 5
    $\begingroup$ Mathematics is a human activity and philosophical considerations necessarily enter the picture. A number of mathematicians are platonic and this helps them doing mathematics. So I would not say that desiring to find the first cause (or a first cause) is necessarily flawed, inasmuch as it stimulates research. Desiring something does not mean that the thing is reachable, we can try to get closer. The mistake is to assume that this first cause actually exists within our material world. $\endgroup$ Mar 20, 2021 at 17:46
  • 1
    $\begingroup$ ''A number of mathematicians are platonic and this helps them doing mathematics'' As an example, if I remember rightly from reading 'The Road to Reality' by Roger Penrose, he explicitly states at the beginning that he is a Platonist (I might be misremembering). $\endgroup$ Mar 21, 2021 at 16:24
  • 1
    $\begingroup$ @TimothyChow: kudos for appropriate Latin phrases. $\endgroup$ Mar 21, 2021 at 18:57
  • 2
    $\begingroup$ Actually it has been translated in English: Conversations on Mind, Matter, and Mathematics, Princeton University Press. $\endgroup$ Mar 23, 2021 at 8:41

Below mathematical logic, there is "everyday logic" - our ability to handle expressions with words like "if", "then", "because", "and", "or", etc., and to build complex arguments from them. Everyday logic is the foundation for mathematical logic and of mathematics in general.

This works because there is a fundamental difference between a real-world proof as it appears in a mathematical book and the "proof" object that occurs in mathematical logic. The real-world proof does not need a formal definition of its logic, it is enough that author and readers agree that all details are right for this specific proof. It is only when we want to talk about all proofs, all formulas, or at least an infinite set of them, that we need a formal definition.

An agreement about a real-world proof is possible because we all have more or less the same everyday logic. And it is similar for all of us because we all live in the same society and have to present and understand more or less complex arguments every day. Another reason is that everyday logic has to map the causal structure of the world we all live in.

And where does this causal structure come from, on which our world, and therefore also our mathematics, relies? Now that is a very good question...


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