AFAIK yes. see the Large Cardinal Axioms (and combinatorial statements!) """ The proposition that such cardinals exist cannot be proved in the most common axio

AFAIK yes. see the Large Cardinal Axioms (and combinatorial statements!) """ The proposition that such cardinals exist cannot be proved in the most common axiomatization of set theory, namely ZFC, and such propositions can be viewed as ways of measuring how "much", beyond ZFC, one needs to assume to be able to prove certain desired results. In other words, they can be seen, in Dana Scott's phrase, as quantifying the fact "that if you want more you have to assume more" """ https://en.wikipedia.org/wiki/Large_cardinal https://en.wikipedia.org/wiki/Large_cardinal And https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof for a similar theme with Peano arithmetic and the epsilon_nought ordinal.