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.
Comments
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.
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.
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.
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.
It really doesn't. 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.
Is not a proof.
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.
Blatantly false, but also irrelevant.
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).
https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
See above.
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.
Was it ever proven for A1-4 in ZF?
Presumably: it's not hard. See e.g. https://math.berkeley.edu/~wodzicki/160/Hilbert.pdf §9:
Just formalise this section in ZF, and it drops right out.