Sorry in advance, the following is quite messy, I didn’t find a way to express myself more clearly and rigorously. I would appreciate suggestions on how to make the following better and try to act upon them as soon as possible. I am by no means claiming my argument is correct, in fact my question is: in what ways is it flawed?
The following notation and terminology is taken from Boolos’s book: “Logic, logic and logic” (chapter 26: a new proof of the Gödel incompleteness theorem, page 383). A sketch is also found in the wikipedia page “Proof sketch for Gödel’s first incompleteness theorem". Here I'll outline some definitions used by Boolos in his proof.
A formula F names the number n iff the following is provable: $$\forall x(F(x)\leftrightarrow x=[n])$$ The predicate $Cxz$ is defined to be true iff an arithmetic formula containing z symbols names the number x. The following predicates are based on $Cxz$: $$Bxy ↔ ∃z(z < y ∧ Cxz)$$$$ Axy ↔ ¬Bxy ∧ ∀a(a < x→Bay)$$$$Fx ↔ ∃y((y = [10] × [k]) ∧ Axy)$$
I would like to make a premise. In my understanding, you can introduce new functions/symbols to create a new formal system (that still behaves exactly like the old one), but with them come new axioms: if you introduce the function/symbol “$+$” and integrate it in your Gödel numbering, you need to introduce some more axioms, such as the couple “$x + 0 = x, x + S(y) = S(x + y)$”, so that you have a function/algorithm to “move” from those axioms and a Gödel number encoding a formula containing just old symbols to another equivalent formula where the symbol “$+$” is encoded (and vice versa). Those axioms have to have a Gödel number. I think at least one axiom needed to define the symbol $A$ would have a Gödel number with an infinite number of digits, therefore not a natural number.
The problem I have with Boolos’s arguments is it seems to me that the formula $F$ is going to instantiate itself infinite times, and therefore its Gödel number would have an infinite number of digits and not be a natural number. I think it is implicitly assumed that the symbol/predicate $A$ can be constructed by using a finite number of the other symbols, and I think this is not true. It’s value seems not definable because of infinite recursion. If so, the proof would be a circular argument: it is assumed the decidability of $A$ (which leads to contradiction) to deduce the decidability of F (which leads to contradiction), but then is deduced F as true and not provable instead of deducing the truth value of $A$ to be not decidable (because $A$ has to be defined by an infinite number of symbols).
You can't say to have a general definition of $A$ until you are able to determine the truth value of any of its instantiations $Axy$. For some $x$ and $y$, the truth value of $Axy$ has to be defined somehow, but its definition/algorithm is necessarily self referential, and falls into infinite recursion. It has to check for number namings (using “name” as defined by Boolos) for every possible formula of less than $y$ symbols, including the symbol $A$, including the possible instantiations of $F$ you can have in less than $y$ symbols. A necessary condition for the truth of $Axy$ is that every single possible formula with less than y symbols does not name $x$, and that has to be verified by the algorithm so that a truth value of $Axy$ can be computed. If the algorithm did not check for formulas containing the symbol $A$, the truth value of the resulting formula would say something about a system of axioms where $A$ is not defined, not about the current one. And it cannot simply be assumed that the old and new system behave the same way anyways: this is something to be achieved as a consequence of a suitable definition of the new symbols. So, $A$ instantiates itself when it checks for instantiations of $F$.
Now, you need to be able to “move” from these formulas containing the symbol $A$ to equivalent ones containing just old symbols, but substituting $A$ in its definition again obviously leads to infinite recursion. Therefore, $A$ cannot be defined by a finite number of symbols that are not $A$, and there is no set of axioms that can move an infinite formula to a finite one in a finite number of deduction steps, therefore $A$ cannot be defined and so the truth value of $A$ cannot be determined, and it seems to me the contrary is assumed in Boolos’s proof.
I feel like this is something along the lines of asking whether the infinite formula “$0=0+0+0+…$” is true. There is no way to exclude a “$1$” will pop up at some point if the number of symbols is not finite. I would say that truth is fundamentally tied to computability in a finite time.
These predicates $A,B,C,$ and $F$ are not new symbols that are being added to the language. Instead, they are merely abbreviations: when we talk about $Axy$, that is merely a shorthand for $¬Bxy ∧ ∀a(a < x→Bay)$, which is in turn itself a shorthand using the definition of $B$. So, there are no formulas including the symbol $A$ that you have to worry about when defining $A$; the language that is used for the formulas referred to in $C$ is just the ordinary language of arithmetic.