The entry on Gödel's incompletenss theorem in Wikipedia says:
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).
My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).
But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?
EDIT
There is a very similar question here.
From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.
So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?
Best Answer
"A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.
"Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]
"Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.
"Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)