Existential arithmetical formula independent of ZFC

Question

In Gödel's incompleteness theorem, the Gödel formula is in the language of arithmetic, so adding it as an axiom changes the properties of $\mathbb{N}$. To me that's already difficult to grasp, because the natural numbers seem a primitive and absolute thing.

Now can the Gödel formula be existential : $\exists n, \varphi(n)$? Now that would not only change the properties of $\mathbb{N}$ but also its contents! If $\exists n, \varphi(n)$ is independent of ZFC, I could pose it as an axiom and get an extra natural number $n$ with property $\varphi(n)$. Would this number be computable, i.e. could we get its explicit sequence of digits? If so, what would happen if I instead pose $\lnot\exists n, \varphi(n)$ and apply that statement to that same explicit sequence of digits?

Answer 1

No, any true existential sentence is provable even in fairly weak theories such as Robinson Arithmetic. So see why, take a true existential sentence $(\exists x) \phi(x)$, where $\phi$ is quantifier free. If such a sentence is true, there is an $n$ such that $\phi(n)$ is true. By induction on the construction of quantifier free sentences, one can easily show that Robinson Arithmetic proves $\phi(n)$. Thus Robinson Arithmetic proves $(\exists x) \phi(x)$.

Answer 2

I am not a specialist in this, so I may be corrected.

The classical Gödel formula is the negation of an existential statement $\lnot \exists n \phi$, which is equivalent to $\forall n \lnot \phi$. It is chosen so that $n$ would be (the Gödel number of) a proof of $\phi$, so in the metatheory we can say that the sentence says $\phi$ is unprovable.

Many people share your intuition that the naturals are a primitive and absolute thing. Unfortunately, in PA and ZFC they are not. It is easy to prove that all the naturals you know and love are there, but you can't prove there aren't any more. The "extra" ones won't have a digit expansion like you imagine, so there is no conflict there with the standard naturals.

The usual proof that there might be more is to add a constant $c$ to the language and the infinite set of axioms $c \gt 0, c \gt 1, c \gt 2, \ldots$. Assuming PA or ZFC is consistent, you can clearly add any finite subset of these axioms and still have a consistent theory. For any finite subset, there is some greatest number that $c$ has to be greater than, so take it larger. The compactness theorem of first order logic promises us that if every finite subset of a set of axioms has a model the whole set has a model. If we have the infinite set of those axioms $c$ cannot be a standard natural, so we know that models with nonstandard numbers exist.