Do any authors systematically distinguish between 'theorems' (which have 'proofs') and mathematical 'beliefs' (which have 'evidence')?

When you dig deep enough, you have to run into belief, or "evidence". The reason is that you have to stop at some point and say to yourself "Okay, my foundations seems somewhat solid. It matches how I think mathematics should be working, even if it's not an extremely well-suited foundations, it does work, as long as I believe in something."

Similarly, you have to wake up and believe that you are alive, and that you exist somehow. You don't have any proof of that. You only have highly circumstantial evidence. Your conscious mind tells you that its getting signals of an outer world, and it thinks that it is alive. But you can never know for sure. If you ever experiment with hallucinogens then you can easily assert the truthfulness of this statement. We conclude that life is out there and we are out there by some relatively long and somewhat consistent stream of input.

Mathematics is the same. You have to believe that if after some stream of input (in the case of first-order logic and $\sf ZFC$ we are talking about nearly a century of very smart people digging into the dirt) that it sounds like a good foundations for the mathematics you are doing. Then you just have to believe that it is consistent, but in that case group theory and the unprovability of commutativity from the basic axioms of group theory, are all granted because we know what is out there.

Of course you are free to feel that first-order logic and $\sf ZFC$ are not good foundations. You are free to choose other foundations. Type theory, category theory, second-order arithmetic, Kripke-Platek set theory, $\sf CZF$, $\sf ETCS$. You can even reject everything else and conclude that mathematics must be based on solid provability which we can actually write down to the last detail and become an ultrafinitist.

But all that is up to you, and the philosophical outlook that you have on mathematics. But you really just have to remember that at some point you really have to stop pussyfoot around this question and start doing mathematics, or else you're not a mathematician you're a philosopher (which is not a bad thing for itself, but it's a whole other thing).


This answer is related to the comments of Andreas Blass above, but I think it more directly addresses the point you're trying to make. Let's use YFFS as an abbreviation for "your favorite foundational system".

The distinction you're making is a valid one. It's stronger to exhibit a formal proof from the group axioms than to prove one exists in YFFS. In the first case, you have the proof, while the second relies on YFFS "telling the truth" about the group axioms and their consequences. This would be an issue if doing group theory was about deriving consequences of the group axioms.

It's not! A group is a mathematical object (a set, together with a binary operation, satisfying the group axioms) living in our imagined mathematical universe (which can be encoded/interpreted in YFFS). A theorem about groups is a theorem of mathematics (which can be formalized in YFFS), about these mathematical objects.

Similarly, number theory is not about looking for formal consequences of PA - it's about using all the tools of mathematics to investigate the properties of $\mathbb{N}$, which is a particular mathematical object.

There are a few reasons to prefer this wholistic approach (proving theorems of YFFS about groups) to the restricted approach (proving theorems of $T_{\text{Groups}}$, the first-order theory of groups):

  1. Most interesting theorems about groups can't be expressed in the first-order language of groups. Okay, as you pointed out in your question that you linked to above, you can move to a different language to capture different scenarios. So to quantify over homomorphisms, you can add a new sort for functions and assert that the things occupying this sort are supposed to be functions etc. etc. But then you have to start from scratch proving theorems in this totally disconnected logical setup - there's no underlying framework to connect them.

  2. Not only are the different situations involving groups disconnected from one another, you also miss out on connections with other areas of mathematics completely.

  3. Proving much of anything directly from $T_{\text{Groups}}$ and its related theories is very difficult, not to mention tedious!

My point is that what you call beliefs are exactly the same things as what most people call theorems (of mathematics), and rightly so.

Now, there are some people who are interested in theorems that are "stronger" than theorems (of mathematics). The project of reverse mathematics is about understanding how much of mathematics (i.e. how much of YFFS, which for reverse mathematicians is usually second order arithmetic) is really necessary to prove a theorem. The less you use, the more robust the theorem, in the way you noted. But this is still using a foundational system, not proceeding directly from $T_{\text{Groups}}$. I don't know much about the automated theorem proving community, but I could imagine that a more restricted setting could be useful here.