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