Some general questions on first-order logic I'm currently working through Peter Smith's 'Introduction to Godel's Theorems'.
I'm wondering how a formalization of first-order logic that allows us to prove the incompleteness theorems, etc. might look. Is it a first-order theory itself? It does appear to make some second-order statements. For instance, when discussing Peano Arithmetic, we want to talk about the set of 'actual' natural numbers, namely the successors of 0 and nothing else. Then again, set theory manages to say things with first order logic which feel more like higher-order logic.
In particular, I wonder if first-order logic can be shown to be consistent itself. If not, what kind of consistence results are there with respect to first order logic?
Thanks.
 A: Take the second question first:

I wonder if first-order logic can be shown to be consistent itself. 

It is a textbook result in any math logic text that a standard deductive system for first-order logic (pick your favourite, axiomatic Hilbert-style, natural deduction style, tableaux-style ...) is consistent. That is to say, you can't derive something of the form $C \land \neg C$ from no assumptions in the deductive system. (Aside: It is perhaps a bit worrying you ask this. I'd really suggest to anyone that they tackle an elementary math logic text which covers this sort of thing before trying to get their head round more advanced stuff like the incompleteness theorems ...) 

I'm wondering how a formalisation ... that allows us to prove the incompleteness theorems, etc. might look. 

To fix ideas, consider (half) the first theorem for first-order Peano Arithmetic, PA. That's the result (F) that if PA is consistent, then PA doesn't prove $\mathsf{G}_{PA}$. This is a result about expressions (wffs) and relations between them, so we need to formalize a theory about expressions. But expressions are finite objects and we can give code numbers for them (that's the trick we use in informally proving (F)). So, using the coding trick, we can in fact express (F) in the language of arithmetic itself. Let $\mathsf{Con}$ be the arithmetical expression that codes that PA is consistent. And the expression that  $\mathsf{G}_{PA}$ is unprovable in PA is -- wait for it! -- $\mathsf{G}_{PA}$ itself. So we can express (F), via coding, in the language of arithmetic as $\mathsf{Con} \to \mathsf{G}_{PA}$.
OK, so what does it take to formally prove this sentence (i.e. to give a formalized proof of half the first incompleteness theorem for PA)? Well, the proof of the first theorem is quite elementary, so you'd expect it to be provable in elementary arithmetic so in PA itself. And it is! [Indeed, as we'd guess, a weak subsystem of PA suffices]. So, in response to your question

First-order PA is itself sufficient to prove (half) the first incompleteness theorem for PA.

Bonus result: Since PA can prove $\mathsf{Con} \to \mathsf{G}_{PA}$ and can't prove $\mathsf{G}_{PA}$, PA can't prove $\mathsf{Con}$. Which is, of course, the second incompleteness theorem.
All this is explained in my book, Ch. 24 in the first edition, Ch. 31 in the much better second edition.
(On a slightly different tack, if you want to know about a formal computer verification of the first incompleteness theorem, then look here: http://r6.ca/Goedel/goedel1.html )
