[pavelrub]

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.

[threatofrain]

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.

[thaumasiotes]

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

[jessriedel]

You guys are basically arguing over Moore's here-is-one-hand problem.

https://en.wikipedia.org/wiki/Here_is_one_hand

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.

[pavelrub]

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.

[ingenter]

There is no pure black in the real world.

[ingenter]

> There is theoretical pure black in any modern representation of color. If the term confuses you, you can replaces it with #000000. If the black vs red comparison still confuses you, you can replace it with #600000 vs #FF0000. You might also want to address my actual argument, instead of irrelevant technicalities.

So you're using a numeric representation of colors (RGB) to prove to me that black is darker than red.

By doing this, you're basically proving my point.

1) different people may have different opinions on "obvious" statements

2) the simpler the statement is, the easier it is to accept or reject it

If you give me two color plates, one is black, and one is red, I might find people who disagree which one is darker.

But if you give me photo measurements, I will say that one is objectively darker with respect to a specific metric (e.g. visible photon energy flux, YCbCr luminosity, CIECAM02 luminosity).

[pavelrub]

> So you're using a numeric representation of colors (RGB) to prove to me that black is darker than red.

No, I’m not doing that at all - I’m simply creating a well-defined understanding between us about which colors we are talking about, so that there won’t be any confusion. If you were sitting next to me, I could show you some other two colors in person, with no reference to RGB or to any other numeric representation, and the exact same argument would stand.

No specific metric can ever show that #FF0000, as it is displayed on any reasonably well-balanced monitor, is darker than #600000. If somebody invented such a metric, we would say that this metric is either incorrect, or misuses the word “darker”. This would also be the case if no other metrics existed before it. Therefore it is clear that our understanding that #FF0000 is darker than #600000 is independent of any formal description of darkness, and comes prior to it.

And you are still avoiding, for some reason, my main argument, which had nothing to do with colors, and dealt specifically with 2+2=4.

[pavelrub]

There is theoretical pure black in any modern representation of color. If the term confuses you, you can replaces it with #000000. If the black vs red comparison still confuses you, you can replace it with #600000 vs #FF0000. You might also want to address my actual argument, instead of irrelevant technicalities.

[thaumasiotes]

How are you getting a "theoretical pure black" without having a rigorous theory of color? If you're just going to call some things black and some things red, you'll find that a lot of things that people call black are lighter than a lot of other things that people call red.

[pavelrub]

I’ve already told you what to do if the term “pure black” causes problems. The color represented by #600000 on my monitor is always darker than the color represented by #FF0000, regardless of the existence of any theory of color. If you claim that some formal theory of color convinced you of that, then it would mean that a different theory of color could conceivably convince you otherwise. But this is clearly impossible: We would say that any theory of color which shows that #600000 is lighter than #FF0000 is simply misusing the word “lighter”. This shows that our understand of what “lighter" and “darker" mean is independent of any theory of color, and in fact this understanding is a precondition for the development of such a theory to begin with.