When you write "I do not see how it could be a function WITHIN first-order arithmetic," it is certainly surprising, but this is in fact the case: figuring out how to internally express the provability predicate is the bulk of Godel's argument. If you actually read the proof, you will see how it is done.
Briefly, the point is that if $\varphi$ is provable from $T$, then there is a certificate for this fact: a (natural number which codes a) proof! A proof is a finite string of sentences satisfying some simple properties, corresponding to the axioms of $T$ and the inference rules of first-order logic. Via Godel coding, it turns out that all relevant statements about proofs can be expressed as first-order arithmetic statements about the codes of proofs.
(Note that this is not true for truth! A certificate for $\varphi$ being true in a structure is a family of Skolem functions, which are second-order objects. There are additional complications as well, but this is the big difference I want to highlight.)
EDIT: A few steps towards understanding the provability predicate:
CLAIM: Peano arithmetic proves "Every finite sequence of 0s and 1s, which has exactly as many 0s as 1s, has even length."
Note that this is silly - the language of arithmetic does not let us talk directly about sequences! Still, we can make sense of this statement via (a silly example of) Godel numbering: to the finite binary sequence $\alpha=a_1a_2a_3. . . a_n$, where $a_i\in\{0, 1\}$, we associate the number $Code(\alpha)=2^{a_1+1}3^{a_2+1}5^{a_3+1} . . . p_n^{a_n+1}$. (Here "$p_i$" denotes the $i$th prime number.) Now, we have:
There is a formula $\varphi(x)$ in the language of arithmetic such that for every numeral $k$, we have $PA\vdash \varphi(k)$ iff $k=Code(\alpha)$ for some finite binary string $\alpha$ with exactly as many 0s as 1s. (If exponentiation isn't in the language of arithmetic, then this is actually pretty difficult! For that reason we often use the conservative extension $PA_{exp}$ instead of $PA$; it's not really any different, but it makes some technical steps easier.)
There is a formula $\psi(x, y)$ in the language of arithmetic such that for every pair of numerals $k, l$, we have $PA\vdash \psi(k, l)$ iff $k=Code(\alpha)$ for some binary string $\alpha$ of length $l$.
Finally, $PA$ proves the sentence $\forall x, y(\varphi(x)\implies \exists z(\psi(x, y)\iff y=2z))$, that is, "Every finite binary string has even length." (This of course depends on the exact choices of $\varphi$ and $\psi$, so the previous two steps really should be made more explicit.)
Note that the above paragraphs take place outside of $PA$, but the formulas $\varphi$ and $\psi$ are formulas of $PA$. There's a deep philosophical issue here: is $PA$ really talking about finite binary strings, or just "simulating" them somehow? (This is closely related to the "Chinese Room" thought experiment of Searle, and many others.) While this is interesting, we're just going to sidestep it: in proving Godel's theorem, we fix a coding scheme, and prove that all the relevant facts - when interpreted by this scheme - are in $PA$. In particular, we get:
A formula $Prov(x, y)$ in the language of arithmetic.
A proof - in the "metatheory" - that, for any pair of numerals $m, n$, we have $PA\vdash Prov(m, n)$ iff $m$ is the code of a sentence $\sigma$ and $n$ is the code of a proof of $\sigma$ from $PA$.
So there is a metatheory here, but its role is interpreting the predicate "$Prov$," not in formulating it. (And, by the way, we can ask what sort of metatheory we need, and the answer is, in a precise sense, "not very much" . . . but that's going a bit too far for now.)
As far as "better examples" go, there are many sentences not obviously of the form "$Con(T)$" now known to be independent of the theory $ACA_0$, which is a conservative extension of $PA$ to a larger language (so there are more things that are expressible - this just makes the examples better). Some examples include:
The Paris-Harrington theorem.
The linear order $\epsilon_0=\omega^{\omega^{\omega^{...}}}$ is in fact well-ordered. (Due to Gerhard Gentzen, who showed that "$\epsilon_0$ is well-founded" implies $Con(PA)$ over a very weak base theory.)
Every two-player perfect information game, which is guaranteed to end after finitely many moves, is determined.
And many more.
If you are interested in this sort of thing, you should check out Reverse Mathematics.
