Do we not need to use the axioms of ZFC for a proof of Gödel's 1st Incompleteness theorem?

Question

The First Incompleteness Theorem of Gödel written in the language of set theory: $$\neg(\exists \beta\in\textbf{Fml})(\textbf{PA}\cup\textbf{FOL}\vdash \beta \land \neg\beta)\rightarrow (\exists G\in \textbf{Sent})(\textbf{PA}\cup\textbf{FOL}\not\vdash G) $$ where $\textbf{PA}\subseteq\textbf{ZFC}\subseteq\textbf{Sent}\subseteq\textbf{FOL}\subseteq\textbf{Fml}\subseteq\bigcup^{\infty}_{n=1}\textbf{L}_{FOL}^n$ and $\textbf{L}_{FOL}=\{\neg,(,),\rightarrow,\forall,v,c,P,*,',=\}$

(where PA is the set of axioms of Peano Arithmetics and FOL is the set of axioms of first order logic as given in Enderton(2001) with their implications, whereas Sent is the set of sentences and Fml is the set of formulas of $\textbf{L}_{FOL}$)

But it seems I need the set theoretic axioms to define, e.g., the set of expressions of L, since when I put $\textbf{Exp}=\{ (\alpha_1,\ldots,\alpha_n) | \alpha_i\in \textbf{L}_{FOL}\}$, I seem to be using the Axiom Schena of Seperation. My argument is that since at least the axioms of ZFC and FOL are needed prove Gödel's theorems, I can at most believe in the truth of the following sentence:

$$\textbf{ZFC}\cup\textbf{FOL}\vdash((\neg\exists\beta\in\textbf{Fml})(\textbf{PA}\cup\textbf{FOL}\vdash \beta,\neg\beta)\rightarrow (\exists G\in \textbf{Sent})(\textbf{PA}\cup\textbf{FOL}\not\vdash G))$$

(Here I am ignoring the circularity problems during the course of the proof such as, that I use ZFC to define Fml and vice versa - since Fml should be included in the axiom schema of seperation. I am also taking the sign ∈ as just another relation in $\textbf{L}_{FOL}$). So, could I conclude that Gödel's Incompleteness for Arithmetics is true only for models of the set of sentences $\textbf{ZFC}\cup\textbf{FOL}$(ZFC1)? Or why is my characterization of these matters is wrong?

Answer 1

See this post for a brief explanation of what is needed for this kind of foundational theorems. Basically, given any formal system $S$ with decidable proof validity that can interpret arithmetic, and any sentence $P$ over $S$, you can construct a sentence $Prov_S(P)$ over $S$ that 'states' that $P$ is provable over $S$. The meaning of "states" here is crucial. If you wish to completely stick to pure syntax, then you would be unable to claim that the sentence $Prov_S(P)$ means anything at all. Only when your meta-system already 'knows' the entire collection of finite strings and all their standard properties (or equivalently natural numbers and PA), can you prove in the meta-system that $S \vdash Prov_S(P)$ iff $S \vdash P$ and that $S \vdash \neg Prov_S(P)$ iff $S \nvdash P$. Note carefully that the notion of "$\vdash$" here is defined based on precisely that collection of finite strings, which is essentially assumed in the meta-system to satisfy the equivalent properties to PA for natural numbers, so it is not at all surprising that $S$ can prove or disprove a statement about validity of a proof (which is a string in the meta-system) since $S$ interprets PA. $ \def\pa{\text{PA}} $

Godel's proof of his first incompleteness theorem depended on the $ω$-consistency of $S$, because he considered $Con(S) = \neg Prov_S(\bot)$, and to show that $S \nvdash \neg Con(S)$ he needed $S$ to be $ω$-consistent. It is necessary because $\pa' = ( \pa + \neg Con(\pa) )$ is consistent and yet $\pa' \vdash \neg Con(\pa')$. Even Rosser's version with a modified $Prov$ cannot even be proven without the meta-system and its 'understanding' of the finite strings.

The internal version of Godel's second incompleteness theorem is often said to mean that PA can prove that it cannot itself prove its own consistency, but this is extremely misleading. What is true is that, from the viewpoint of the meta-system, $\pa \vdash Con(\pa) \to \neg Prov_\pa(Con(\pa))$. It is true that we can write down the whole proof in PA, and one can check that it really is valid over PA, purely syntactically, but if you don't have a meta-system then it remains a totally meaningless theorem and proof.

The only surprising thing is that PA (or even Robinson's Q) is strong enough to handle arbitrary finite string manipulation. That is the most important contribution of Godel. But for really not much is needed in the meta-system, not to say set theory! (See this announcement of a proof of Godel's incompleteness theorems in Isabelle, for example.)