What would provable existence of a non-standard natural number imply about ZFC?

Question

Assume that in ZFC we can define a set $x$ in some way and that the following are provable:

1. $x$ is a finite ordinal, (i.e. $x\in\omega$)
2. $x\neq0$
3. $x\neq1$
4. $x\neq2$
5. etc.

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)?

Answer 1

It sounds very unlikely that an argument such as the one you're envisaging can be made.

Namely, if ZFC is consistent, then there exists a consistent extension of ZFC where an $x$ with your properties is definable. More precisely, thanks to Gödel and Rosser, there is a primitive recursive function $f$ such that $\exists y\in\omega.f(y)=0$ is independent of ZFC, and if we add this as an axiom, then we can define $x$ as the least such $y$, and prove $x\in \omega$ (trivially) and also $x\ne\overline n$ for every numeral $\overline n$.

(Note, by the way, that in this case there is an algorithm that proves all of the $y\ne \overline n$ statements uniformly -- just trace the computation of $f(\overline n)$ and format that as a proof).

So if your argument is possible, then it would have to show, not that an $x$ with the properties you imagine can't exist, but that ZFC, specifically, is too weak to prove its existence.