[pavelrub]

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.

[mcguire]

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.

[1] https://en.wikipedia.org/wiki/Principia_Mathematica

[pavelrub]

> 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 the proof of 1+1=2 is itself trivial in PA. So this really doesn't mean much. In fact it seems like you are agreeing with me that having explicit proofs of m+n=l for m,n>1 is meaningless.

> 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

I understand your point, but saying that there might be an occasions where a proof of P can be meaningful is not the same as saying that a proof of P is meaningful. The former is almost a tautology, and can be said about practically any proof whatsoever.

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

This doesn't show that those proofs are meaningful in mathematics.