I’m interested in understanding the logical structure of mathematics – I want to know how it all fits together. To this end, its interesting to ask whether any authors systematically distinguish between ‘theorems’ (which have ‘proofs’) and what we might call mathematical ‘beliefs’ (which have what we might call ‘evidence’).
Let me try to explain the difference. By the way, this question is inspired by Peter Smith’s answer here and Asaf Karagila’s comment thereunder.
We’ll use the following example. Begin with the group axioms, and for good measure, lets throw in the assumption that the domain of discourse is infinite (thereby obtaining the ‘infinite group axioms’). We can do this by adjoining a new function symbol $S(*)$ together with the following axioms.
Okay, that will be our example. Now lets get to the point.
Observe that the following is a theorem of the infinite group axioms: ‘for all $x$ and all $z$, there exists $y$ such that $xy=z$.’ Furthermore, we know its a theorem because it has a formal proof from the axioms.
Now consider the following statement: ‘for all $x$ and all $y$ we have $xy=yx$.’ Almost nobody believes that this is a theorem of the infinite group axioms – surely there exist infinite groups that are not Abelian! Thus, the sentence ‘commutativity cannot be deduced from the group axioms’ is a belief. And, different people will offer different evidence in favor of this belief.
For instance, I might proceed as follows. First, I formalize the statement that ‘commutativity cannot be deduced from the infinite group axioms’ in the language of set theory. Then, I prove it using ZFC, perhaps by constructing an infinite group that is not Abelian. Or perhaps using other means. In any event, I have used the ZFC axioms to prove the formalized-in-the-language-of-set-theory version of the statement ‘commutativity cannot be deduced from the infinite group axioms.’ So, this is evidence for my belief. But, it is not proof of that belief. After all, ZFC might be inconsistent, or even if its consistent, nonetheless it may prove statements about arithmetic that are false. So I repeat, this is ‘merely’ evidence. And, someone may produce stronger evidence, perhaps by appealing to only a fragment of the ZFC axioms, or perhaps by formalizing the statement ‘commutativity cannot be deduced from the infinite group axioms’ in the language of arithmetic and proving it using only PA. If they’re able to do this, then their evidence is stronger than mine.
So whereas all proofs are, in some sense, equally good, the same cannot be said of evidence. Not all evidence was made equal. If you appeal to a weaker theory, then your evidence is stronger. Of course, there’s a socially determined cut-off point beyond which nobody will doubt your evidence. That’s fine – we’re still better off calling it ‘evidence,’ rather than ‘proof’, as I argue below.
Okay, so that’s the idea. But, do any authors purposely and systematically make this sort of distinction? And, does it help clarify the logical structure of their writing? Also, if any logicians or philosophers of mathematics have written about this sort of thing, I’d be interested in reading their stuff.
Addendum. It is tempting to argue that, if we prove the consistency of a first-order theory using a sufficiently weak foundations, then this is more than just evidence of its consistency, it is proof. We might therefore try to reclassify certain beliefs and start calling them theorems.
There’s at least 2 reasons to fight this temptation.
Firstly, I don’t think there’s a clear place to draw the line between safe and risky foundations. Thus, I don’t think there’s a clear place to draw the line between beliefs that must remain beliefs, and beliefs that we’re so sure of that we can start calling them theorems. So, instead of trying to find the perfect location for this hypothetical line, and then dogmatically forcing our somewhat arbitrary decision upon others, I think we’re better off just leaving beliefs and theorems as separate concepts.
This brings me to my second point, which is this. Proving a theorem is methodologically different to accumulating evidence in favor of a belief. In the former case, we can immediately begin trying to prove the theorem of interest directly from the axioms. Whereas in the latter case, we must first choose a foundational theory in which to proceed, we must formalize our belief as a sentence in the language of that theory, and only then do we begin trying to prove something.
Thus, I contend that the crucial difference between beliefs and theorems is not how certain we are of their truth; but rather that, methodologically, we deal with them differently. Hence the possibility that emphasizing the belief/theorem distinction could help to reveal the deeper logical structure of mathematics, which is what I’m interested in.
By the way, the word ‘belief’ isn’t a great fit for what we’re meaning here. Perhaps it would be better to call them ‘blurgles’ to avoid this issue. So under this view, theorems have proofs, and blurgles admit evidence.
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):
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.
Not only are the different situations involving groups disconnected from one another, you also miss out on connections with other areas of mathematics completely.
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.
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).