what is the proof-theoretic strength (largest ordinal whose existence can be proved) for ZFC set theory?
What? All I can do is make the obvious guess, and I'm not even sure that's well-defined, let alone the answer you seek.
The obvious guess would (IMHO) be something like the supremum of all of the ordinals in the constructible hierarchy.if the smallest ordinal that can't be proven is well-defined: what is the guess?
And that's where the extent of my knowledge ends. Although now that I think about it, the continuum hypotheses probably tells us some interesting information.Perhaps it isn't well defined. What is known, then, about the supremum of the set of definable ordinals in ZFC, and the infimum of undefinable ordinals in ZFC?