Top-down mathematics, or "Where it all begins"

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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...