Assume that in ZFC we can define a set $x$ in some way and that the following are provable:
- $x$ is a finite ordinal, (i.e. $x\in\omega$)
So to say that the existence of a non-standard natural number was provable. If ZFC was inconsistent, this would certainly be possible. My question is, if we had such an $x$ for which the list of statements was provable, would this in turn imply that ZFC is inconsistent? Would consistency of ZFC still be possible given that there is no algorithm which could effectively prove all the statements (This is what I would conjecture)?