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

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?

• The incompleteness theorem can be stated and proved without needing set theory -- Peano Arithmetic is (more than) sufficient. You would need to believe that the arithmetical formulas that express provability actually capture your intuitive concept of "provable", but that is not different in principle from the situation when you use set theory to model provability instead. – Henning Makholm Oct 17 '16 at 12:10
• @HenningMakholm PA can't even state what is meant by provability or incompleteness, the statement doesn't seem correct. I think the issue is in the "you would need to believe" part, so you would need a meta-language strong enough to convert the beliefs into proofs. – Dole Dec 21 '18 at 11:13

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.