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