> This proof showed that “1 + 1”, does indeed equal “2”. It took 2 volumes to get here.
I know this seems logical to mathematicians, but it feels to me like having to take 2 volumes to prove something than any child knows intuitively is... I don't know what word I am looking for... obsessive?
You can imagine "1 + 1 = 2" not as an important question in this context, but rather a proof of concept for the system they devised. It's a bit like the story about a "black triangle" [0]: a rather useless model passed through a rendering pipeline to produce a result any OpenGL novice can scramble in a couple dozen lines, but showing that the whole pipeline does, indeed, actually work as intended.
The point is not to prove that 1+1=2. The point is to construct mathematics (all of mathematics) directly from the axioms using a formal language. The objective of 1+1=2 is not interesting, but the result is a rigorous foundation of mathematics using formal languages.
The upshot is twofold: (1) we have a rigorous foundation of mathematics in formal logic which CAN be used to prove nontrivial statements, as in the application of model theory to mathematics, and (2) we can now build proof assistants that allow us to use computers to better understand proofs.
Both applications of formal reasoning are equally interesting and have wide ramifications in mathematics.
The idea is that 1+1 proof is made without the mathematical apparatus(High-level language) available after 1+1, i.e. its like a huge Assembler bootloader made from verified primitives(logical primitives) to load an operating system with High-level API(Mathemathics).
They didn't set out to explicitly prove 1+1=2, they just got around to it after 2 volumes, it didn't require 2 volumes of background. A direct proof of 1+1=2 is pretty short in most logical systems.
I know this seems logical to mathematicians, but it feels to me like having to take 2 volumes to prove something than any child knows intuitively is... I don't know what word I am looking for... obsessive?