2+2=4 is obvious. The axiomatic proofs are mostly a meaningless and boring exercise that mathematicians invented when they wanted to axiomatize everything. They have nothing to do with whether something is obvious or not. It isn't as if it was possible to doubt that 2+2=4 before the invention of the Peano axioms.
There's a lot of historical context you're missing if you think axiomatic proofs are meaningless. Around the late 1800s, a few contradictory proofs started popping up because people weren't being rigorous enough (the example I know involved proofs about pointwise vs uniformly continuous functions just being referred to as "continuous"). Then a few paradoxes were discovered (like Russel's paradox, the set of all sets that don't contain themselves) and the Mathematics community realized formalizing their assumptions and reproving everything from the ground up was necessary. So Whitehead and Russel started to write Principa Mathematica, and everyone was happy in the Math world until Godel came along and proved that Principa Mathematica would either have contradictions or have unprovable theorems.
I think I wasn't clear enough. I never meant that axiomatic proofs in general are meaningless, only that axiomatic proofs of trivial arithmetic facts (1+1=2, 2+2=4...) are meaningless.
1. You assume "trivial arithmetic facts" as axioms.
Result: You have an infinite number of axioms. (Whee!) The likelihood that you have snuck in non-trivial assumptions is pretty high, unless you are very strict about how you define "trivial" (which is probably as much work as just proving the trivial facts), and in that case, there's a high probability that some of your trivial facts are false.
2. You demonstrate that you can prove "trivial facts" in your system and you do so when needed by more complex proofs. The proofs of trivial facts are not necessarily trivial.
In neither case is your handling of "trivial facts" meaningless.
From a mathematical point of view, one must be very careful, and we have abundant evidence of that.
However, we are fully justified in saying that if anybody came up with a mathematical system in which 2 + 2 != 4, we can dismiss it without having to do some sort of deep analysis of it. 2 + 2 = 4 is obvious. We can literally do it with 4 little objects right in front of us. If we can not accept that as obvious, we are hopelessly ignorant and have no reason to trust our fancy proofs, either. (Italicized to emphasize my main point.) If you can't trust that, you certainly can't trust the significantly more complicated number theory axioms do anything useful.
Note that 2 + 2 = 4 carries some implicit context when we say it without qualification, and subtly sliding in a context change is not a disproof. 2 + 2 = 1 modulo 3, but that's not what anybody means without qualification. Clearly we're operating on "the numbers I can hold in my hand" here, or some superset thereto. Note how I'm not even willing to say "the natural numbers" necessarily; it isn't obvious to me what some billion digit number added to some other billion digit number is. It's actually crucial to my point here that I'm not extending "obvious" out that far; I can only run an algorithm on that and trust the algorithm. But I'm just being disingenuous if I claim ignorance of 2 + 2. And being disingenuous like that tends to turn people off, and doesn't encourage them to try to learn more.
Let's say I have a new mathematical system (that I call the "brontosaurus"). It is made up of some fundamental elements ("a little end", "a big part in the middle", and "another little end") and some axioms ("and that's how dinosaurs are shaped"). Now, I claim that this is a complete formalization of all mathematics, such that if you prove some statement S involving quaternions, tesseracts, and turgid verbals, you can be assured that no falsehoods have crept in and therefore that S is true.
But in my system, it's not immediately apparent whether 2+2=4, if only because none of '2', '4', and '+' are part of the fundamental elements. So, how are you going to determine whether my system claims 2 + 2 = 4 or 2 + 2 != 4? You'll need to prove it, one way or the other (or both, in which case my system is screwed).
The proof that 2+2=4 has absolutely nothing to do with "claiming ignorance" and everything to do with whether or not you can "trust the algorithm".
Okay. So according to you, the explicit proofs of the following facts, using the Peano axioms, are all meaningful for mathematics:
1. 2+2=4
2. 3+2=5
3. 3+3=6
4. 4+3=7
5. 4+4=8
Is there any serious mathematical work that explicitly proved them all? Have those proofs influenced mathematics in any meaningful way, or in any way at all? Did they demonstrate something that we didn't know before?
I might agree that a single demonstration of something like 1+1=2, using the Peano axioms, might be educational (though not necessary) for somebody who tries to understand the axioms, but to claim that in general those proofs are meaninfull is simply false. A thousand-page book filled with proofs of n + m = l type statements will contribute absolutely nothing to mathematics.
Well, according to the Wikipedia page on Russell and Whitehead's Principia Mathematica[1], "54.43: "From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." —Volume I, 1st edition, page 379. (The proof is actually completed in Volume II, 1st edition, page 86, accompanied by the comment, "The above proposition is occasionally useful." - they go on to say "It is used at least three times, in 113.66 and 120.123.472.")" So that proof has been used on at least three occasions.
No, there are no books (that I know of) containing explicit proofs of "n + m = l" for all n and m up to some values. There wouldn't be any point: if you can prove 1+1=2 at all, then the generalization to n+m=l (where l is the "intuitive" value of n+m) should be easy enough to use directly. But my point is that, if you are constructing a proof in formal mathematics and find yourself at a step having to demonstrate 4+4=8, you have to either (a) assume 4+4=8 or (b) prove that 4+4=8, either manually or invoking some previous lemma or some such. There are no other choices. And option (a) seems to imply that you have an infinite number of axioms, at least one for each possible n+m=l---and that's kind of frowned upon in formal mathematics.
Think of it as a programming problem. (Formal mathematics and programming have a great deal in common.) The required output includes the line
n = 4
when n = 4. You explicitly have to print "n = 4" somehow, either by invoking
printf("n = %d\n", n);
or by writing a function to print the decimal value of a variable or by having a big table of
"n = 0",
"n = 1",
...
for all values of n and printing the appropriate string from that list. You don't have the option of saying "That's trivial" and going on without doing anything.
Now, as for whether this kind of formalization, which necessarily makes all the details explicit, has any influence, I'm the wrong person to ask. I suggest Gottlob Frege, David Hilbert, Russell and Whitehead, Kurt Gödel, or Turing.
For me, I just have to note that all of the dependently typed programming languages I've played with have used Peano arithmetic for encoding the size of an array in the type system. As a result, the requirement of a proof that n+m=l (where l is the "intuitive" value...) has been encoded in the type of, say, array concatenation.
Given the Peano axioms, yes. But most attempts at a formal axiomatization of mathematics don't start from Peano. (If you start from arithmetic, you may have difficulty proving set theory.) Frege started from Cantor's naive set theory, which blew up in his face. Russell and Whitehead[1][2] finally started from formal logic and some weird typed version of set theory that no one has ever explained to me and thus that I fear with superstitious dread. And that takes somewhere over 300 pages to get to "1+1=2", and the proof isn't actually completed until page 86 of volume 2 (according to Wikipedia).
Further, that the fact is trivially provable from Peano's axioms still doesn't mean the proof is meaningless.
I believe you're mistaken. There is value in axioms and axiomatic proofs: two different people will most definitively have a different notion of "obvious", and even have a different understanding of a mathematical problem. So a proof may be accepted by one person and rejected by another.
Given a set of axioms and proofs it's possible to mechanically check a proof. It's not quite possible to reliably check proofs otherwise.
I'm not saying anything about the ability to check proofs, or the value of axiomatic proofs in general, only that 2+2=4 specifically doesn't require an axiomatic proof in order to convince anybody that it is true. This is like saying that we need a rigorous theory of color in order to be convinced that black is darker than red. Mathematicians didn't axiomatize natural numbers in order to show that 1+1=2 or 2+2=4, or any other trivial arithmetical fact. They have never doubted it, and I don't know what "doubting 2+2=4" even means. In fact the entire process is reversed: they invented axioms that can form a formal basis for what we already know to be true. If Peano axioms proved that 2+2 = 6 - they wouldn't be a valid axiomatization of the natural numbers. One cannot axiomatize the natural numbers without already assuming that all the basic arithmetic facts we know about them are true (or else he wouldn't be axiomatizing the natural numbers, but something else). Somebody who rejects 2+2=4 has a problem understanding human language, not proofs.
I feel like this kind of attitude belies that everyone has a different idea of obvious, and that this kind of self-assured confidence is what froze geometry until about 100 years ago.
Realizing that axioms were switches to be turned on and off to generate new structures that may or may not be useful was an important step to abandoning the most obvious and intuitive truths of geometry. Thus geometry has no concept of true outside of axioms, and true simply means internally coherent. Outside of formalization, "obviously true" is the hindrance of confidence.
> This is like saying that we need a rigorous theory of color in order to be convinced that black is darker than red.
You do, if you want to be right. The fact that you can get people to agree with you doesn't make you right, and red is frequently darker than black by some pretty normal definitions of "darker". Red and black are differentiated by the shape of their reflective spectrum, not the amplitude.
pavelrub's point is that you sometimes have less reason to believe the axioms of your formalization than their derived consequences. We have better reason to believe the intuitive idea that 2+2=4 than we do any putative axioms of arithmetic. If we derived that 2+2=5 from some particular axioms of arithmetic, we would conclude those axioms were wrong (or rather, were not the proper system for formalizing 2-plus-2-ness) rather than conclude that 2+2=5.
Pure black is never lighter than any shade of red, by any definition of "dark" or "lightness" that I'm aware of. The point here is that again the words "dark" didn't come into language from some rigorous theory of color - the process is reversed. A theory of color can never show that red is darker than black, because this would simply be a misuse of the word "darker", in the same way that no valid axiomatization of the naturals can possibly show that 2+2 != 4.
But are people more likely to accept the axioms of Principia Mathematica (and the soundness of every logical step from page 1 to 300) than they are to accept the notion that 2 + 2 = 4 based on intuitive notions of what twoness, fourness and plusness are?
Of course they are more likely to believe their intuitions. They also believe that it makes no difference whether or not you swap doors in the Monty Hall problem, and don't believe that with only 23 people the odds of a shared birthday are more than 50%.
To some extent, there is the problem. People trust their intuitions, and their intuitions are often wrong. That's why for some things we need proper proofs.
But proofs always come back to axioms, and on what basis do we accept axioms? That they sound intuitively right. So we've just kicked the problem upstairs a bit, we can't avoid using our intuition.
Personally I'm more likely to believe 2 + 2 = 4, something I can easily check to my own satisfaction using four objects, than I am to believe the Axiom of Choice.
We still use our intuitions, but now everyone knows the starting set of assumptions.
As for the axioms in use, I think the big reasons they were chosen is: They lead to results we already wanted/proved to be true.
Another thing to keep in mind, not everyone works with the same sets of axioms. Which, as someone with a formalist[2] view on mathematics, I find interesting. For example, not everyone studying logic assumes the principle of the excluded middle[1]. One of the consequences of this is that you can no longer do proofs by contradiction.
The axiom of choice is another example of this where two groups of mathematicians accept it or not. I'm a formalist, so I don't have issues with this (as long as both sets of axioms are interesting and "intuitive"), other philosophies of maths might.
It comes down to levels of assurance. The rules of inference you are using are part of your design space. Mathematics at its core is about clever problem solving. When you encounter a problem you have to decide what you would accept as a proof, and this forces you to accept certain reasoning principles.
The caveat is that this is non-trivial and it's very easy to make people accept assumptions which are completely wrong. That's really the main reason to accept the axioms of set theory: People have been trying to poke holes in them for a hundred years and nobody has managed it yet. If you can use set theory (or something equiconsistent) to solve your problem, chances are that nobody will be able to call you out on a mistake.
Well, the whole idea is to pick simple axioms, so it's harder to get wrong. And also, every successful prediction that math makes based on the axioms, is in a sense a verification of them.
> It isn't as if it was possible to doubt that 2+2=4 before the invention of the Peano axioms.
It certainly was; primitive cultures frequently lack words for medium-high numbers like 10, and have been known to lack 4. Unsurprisingly, those people are generally uncomfortable when asked to manipulate quantities that high. (They may use other methods, like having a collection of stones which is known to match the number of sheep in a flock, and "counting" sheep as they arrive by moving a stone from one pile to the other. If you failed to move a stone, you're missing a sheep.)
Not having a word for 4 and doubting that 2+2=4 aren't the same thing. The former means that you cannot understand what the proposition means, while the latter means that you do understand what it means, but aren't convinced that it's true.
[1] https://en.wikipedia.org/wiki/Principia_Mathematica