I've found a machine-verifiable version of the Banach-Tarski proof for the Coq proof assistant. It looks endless. I first thought that this is because the Coq formalisms are excruciatingly lengthy, but the classical, annotated first-order-logic version is also 30 pages long. — alcontali
You hit a lot of really cool topics. I'll keep my answers brief. I hope we can focus on one or two things instead of branching out into too many diverse topics. You uptake new information rapidly but have a hard time staying focussed. Is that a good guess?
* Now re Banach-Tarski. First, a machine-formalizable proof would not be remotely understandable to a person who didn't already understand the standard proof. So that's not the way to go. Coq and machine-assisted proofs in general are an interesting subject, but let's hopefully
not get sidetracked into that.
To that end, you should definitely read the
@Mephist I linked earlier. He knows a lot more about Coq and constructive math than I do if he's around.
Secondly, it turns out that the proof of Banach-Tarski is very straightforward. The outline on Wiki is very good. And as I said, it is at heart a
syntactic matter that could be programmed into a computer. Not the entire proof, but the core idea. If you are interested, the key buzzphrase is: "The free group on two letters has a paradoxical decomposition." That phrase leads to a web of interrelated Wiki pages that are very good. You'll halfway understand B-T from those.
But you know -- the fact is that Banach-Tarski is at heart a logical paradox. You lay out some very sensible axioms, and they lead to a non-sensible yet logically correct conclusion. Tarski and von Neumann and others were all interested in applying group theory to geometry. So this is a paradox in "geometric group theory." That's yet another buzzwordy way to say it. But Tarski was in the middle of all that.
It uses pyramidal vocabulary. For example:
Theorem 22 (Tarski’s Theorem)Let G act on X, and let E ⊆ X. Then there exists a finitely additive, G-invariant measure on X defined for all subsets of X and normalizing E if and only i fE is not G-paradoxical.
So, it requires figuring out what "G-invariant measure" and " normalizing" means. Otherwise, Tarski's theorem 22 will remain inaccessible. — alcontali
No no no!! It's not NEARLY so bad. I could fully explain the proof of the Banach-Tarski theorem to you in a perfectly understandable way. Just not here, because it's a little lengthy. There are several moving parts. But each part of the proof is
quite straightforward.
You don't have to make your life difficult by wondering what those buzzwords mean. You could ask me, for example. But not in this thread. If someone starts a B-T thread that would be more appropriate. But the buzzwords are easy once they're explained.
The think about the Tarski theorem you quoted is that professional mathematicians can always summarize the proof in a sentence or two of jargon. The idea isn't to understand the jargon from the top down. You can understand the proof from the basic ideas on up. It's long but each part is surprisingly straightforward.
I can tell you want the buzzwords mean, but they won't shed light on the paradox until AFTER you understand the paradox. Tarski's using professional jargon.
It is interesting, though. If the proof were about formal language, I would probably keep drilling down in order to figure it out. — alcontali
I could lay that out for you in a page of exposition. Start a new thread, I feel bad enough about hijacking this one.
The heart of the proof is about formal language. It's about all the finite strings you can make using two symbols and their inverses. It is the most syntactic thing you ever saw. It's a very natural construction that contains a surprising paradox. We then apply the paradox to Euclidean three-space.
But nevermind, this is not a forum for lengthy mathematical exposition. You can just google "Free group on 2 letters paradoxical" and there are a bunch of interrelated Wiki pages. That's probably better than my posting an exposition here.
Actually, Tarski does have theorems in the realm of formal languages, e.g. his undefinability theorem. I wonder how he ended up also working on abstract algebraic geometry and topology? — alcontali
These days logic is geometry. It's all come out via the mysterious categorical point of view. Buzzword: "topos theory."
But a lot of these old guys did a lot of different things.
Hilbert is also like that. He did his language-oriented Hilbert calculi but also his geometry-oriented Hilbert spaces. I wonder how people manage to not only handle both domains but even be original in both? — alcontali
Hilbert did much more than that. He's regarded as the number one mathematician of the first half of the 20th century. (Grothendieck wins the second half). He almost beat Einstein to general relativity. He's famous for a lot of deep work in a lot of areas. Very interesting guy, I'm sure you've seen the famous picture of him in his hat.
There could actually even be a deeper link between geometry and formal language, because the late Voevodsky saw homeomorphisms everywhere in formal language domains, while those are clearly a geometry concept. I still don't understand Voevodsky's univalent foundations. Everybody seems to be raving and hyping that stuff, but I still cannot wrap my head around it. — alcontali
That's something else I could put in context for you in fifteen minutes, but not this fifteen minutes. Make a thread so we don't go in all directions here.
There is of course nothing more fashionable than being able to come up with a finer point in the Voevodsky stuff. I cannot "show off" because I unfortunately don't get it! ;-) — alcontali
I hope you will allow me to a suggestion. It's not about showing off. It's about learning. You happen to be interested in a lot of things I know a little about (and some I know a lot about). I'm happy to yack about them. I'm pretty ignorant about most other things. Ask anyone.
There's a Zen saying. Beginner's mind.