This is a fabulous result, both positive and negative, for many reasons. But one of the things people don't realise is that there is a reason why it's interesting mathematically and not just a gimmick.
In Classical Euclidean Geometry there are five axioms, and while the first four seem clear and obvious, the fifth seems a little contrived. So for centuries people tried to prove that the fifth was unnecessary and could be proven from the other four.
These attempts all failed, and we can show that they must fail, because there are systems that satisfy the first four, but do not satisfy the fifth. Hence the fifth cannot be a consequence of the first four. Such systems are (for obvious reasons) called Non-Euclidean Geometries.
So we can use explicit examples to demonstrate that certain proofs are impossible, and the Banach-Tarski Theorem is a result that proves that a "Measure"[0] cannot have all four obviously desirable characteristics.
For more information, here's a blog post[1] I wrote some time ago:
It's intended to be readable, but the topic is inherently complex, so it may need more than one read through. If you're interested.
[0] Technical term for a function that takes an object and returns a concept of its size. For lines it's length, for planar objects it's area, for 3D objects it's volume, and so on.
Nice write-up, though I wish you had expanded a bit more on this:
"We can show that using the axioms of Zermelo-Fraenkel Set Theory we cannot prove the product of an infinite collection of non-empty sets to be non-empty. That seems daft..."
Indeed, and it's exactly the sort of thing that you should not simply proclaim to be true with no explanation or reference.
>> "We can show that using the axioms of Zermelo-Fraenkel Set Theory we cannot prove the product of an infinite collection of non-empty sets to be non-empty. That seems daft..."
> Indeed, and it's exactly the sort of thing that you should not simply proclaim to be true with no explanation or reference.
I'll see if I can hunt out an accessible reference. Problem is, I think it uses Cohen's forcing, and that's pretty tough going in any kind of detail. I might add a note ... thanks for the suggestion.
You don't have to give a full proof, just an intuitive explanation of why the "obvious" arguments fail. For example, we can prove the non-emptiness of product sets for finite sets. Why can that not simply be extended in the "obvious" way to infinite sets? How can making the sets "bigger" suddenly make the product empty?
The problem I have is that "intuitive arguments" differ between people. What one person thinks is intuitively obviously true, another can think is intuitively obviously false.
I'll have to think about what I would be trying to say.
It's a good point ... it's now explicitly on my list.
>So we can use explicit examples to demonstrate that certain proofs are impossible
Nonsense. The independence of an axiom shows in general nothing about what you can and can not prove. A statement can just be false and therefore unprovable.
If you want an actual example of an impossible proof you want to look at the continuums hypothesis. With is probably unprovable and probably unable to be disproven.
>Banach-Tarski Theorem is a result that proves that a "Measure"[0] cannot have all four obviously desirable characteristics.
The important point is that it can't have these properties on all sets. If you restrict yourself to specific sets, these properties can be achieved. E.g. it is false that you can separate a sphere into countable Lebesgue measurable sets which can be rearranged to form a set with larger Lebesgue measure.
>> So we can use explicit examples to demonstrate that certain proofs are impossible
> Nonsense. The independence of an axiom shows in general nothing about what you can and can not prove. A statement can just be false and therefore unprovable.
You clearly know about these things, but I think you have not seen my intended meaning. It's easiest to use the example of Euclidean Geometry to clarify.
We have axioms A1, A2, A3, and A4. We want to prove A5 from these. But we can show that it is impossible to do so by creating a system (for example, spherical geometry) wherein A1, A2, A3, and A4 are all true, but A5 is false. The existence of this system then shows that A5 cannot be proven from A1, A2, A3, and A4.
Thus the explicit example of spherical geometry shows that it is impossible to prove A5 from A1, A2, A3, and A4.
I wonder if your deeper knowledge of the subject is leading you to expect more of my statements than what I'm actually saying.
>> Banach-Tarski Theorem is a result that proves that a "Measure"[0] cannot have all four obviously desirable characteristics.
> The important point is that it can't have these properties on all sets.
Yes, that is one of the four desirable properties.
* Measures 1 on the unit object;
* Countably additive;
* Isometry invariant;
* Defined on all sets.
We can't have all four of these, even in one dimension. But if we relax "Countable Additivity" to "Finite Additivity" then we can have all four properties in one dimension, and in two dimensions. What the Banach-Tarksi Theorem shows is that even with the relaxation in property two of Countable to Finite, in three dimensions we still can't have a measure with all four desirable properties. That's why we don't relax that property, we relax property four, and no longer require the measure to be defined on all possible (sub)sets.
> In general case given a system it is impossible to prove it is not self-contradictory.
If you're asserting it, by merely asserting axioms, then (in the general case,) yes. If you're constructing it, and showing that the axioms are satisfied, then no: there are several ways to construct a model that nobody has ever found a contradiction in, and you can construct spherical geometry this way.
> It really does. The existence of a system where A1-4 are true, but A5 is false proves that you can't conclude A5 from A1-4.
No it does not. First you'd need to show that your A1-4 == true, A5 == false system is not self-contradictory. Cause if it happens to be you basically proved A5 by contradiction (assuming A1-4).
It's impossible to prove that a (sufficiently-strong) system is consistent in that system. It's perfectly possible to prove that many systems are consistent with respect to the consistency of (say) ZF, and ZF's consistency isn't controversial.
All proofs are, ultimately, proofs to one's satisfaction, so bringing Gödel's incompleteness into this isn't insightful, imo. It's like bringing up the Problem of Induction in a discussion about science: yeah, you're right, but now we're not talking about the interesting thing any more.
> The axioms, which we have discussed in the previous chapter and have divided into five groups, are not contradictory to one another; that is to say, it is not possible to deduce from these axioms, by any logical process of reasoning, a proposition which is contradictory to any of them. To demonstrate this, it is sufficient to construct a geometry where all of the five groups are fulfilled.
Just formalise this section in ZF, and it drops right out.
In Classical Euclidean Geometry there are five axioms, and while the first four seem clear and obvious, the fifth seems a little contrived. So for centuries people tried to prove that the fifth was unnecessary and could be proven from the other four.
These attempts all failed, and we can show that they must fail, because there are systems that satisfy the first four, but do not satisfy the fifth. Hence the fifth cannot be a consequence of the first four. Such systems are (for obvious reasons) called Non-Euclidean Geometries.
So we can use explicit examples to demonstrate that certain proofs are impossible, and the Banach-Tarski Theorem is a result that proves that a "Measure"[0] cannot have all four obviously desirable characteristics.
For more information, here's a blog post[1] I wrote some time ago:
https://www.solipsys.co.uk/new/ThePointOfTheBanachTarskiTheo...
It's intended to be readable, but the topic is inherently complex, so it may need more than one read through. If you're interested.
[0] Technical term for a function that takes an object and returns a concept of its size. For lines it's length, for planar objects it's area, for 3D objects it's volume, and so on.
[1] In case people want to discuss that separately I've submitted it as a separate post here: https://news.ycombinator.com/item?id=40798224