The arithmetized completeness theorem In Kikuchi's paper Kolmogorov complexity and the second incompleteness theorem he states the "arithmetized completeness theorem" as follows:

Let $T$ be a recursively axiomatizable theory in a language
$\mathcal{L}$, $C$ be a set of new constants and
$\overline{\mathcal{L}}=\mathcal{L}\cup C$. We say a formula $\phi(x)$
in $\mathcal{L}_{A}$ defines a model of $T$ in a theory $S$ in
$\mathcal{L}_{A}$ if we can prove within $S$ that the set
$$ \{ \sigma : \text{$\sigma$ is a sentence in $\overline{\mathcal{L}}$ that satisfies $\phi(\ulcorner\sigma\urcorner)$} \} $$
forms an elementary diagram of a model of $T$ with a universe from
$C$.
Theorem 4.1. (The arithmetized completeness theorem). There exists a formula $\text{Tr}_{T}({\ulcorner}x{\urcorner})$ in
$\mathcal{L}_{A}$ [the language of arithmetic] that defines a model of
$T$ in $\text{PA} + \text{Con}(T)$ , where $\text{Con}(T)$ is a
sentence in $\mathcal{L}_{A}$ that means $T$ is consistent.

There are several aspects of this theorem I don't understand:

*

*The notion of a formula defining a model of $T$ in $\text{PA} + \text{Con}(T)$ involves the set $ \{ \sigma : \text{$\sigma$ is a sentence in $\overline{\mathcal{L}}$ that satisfies $\phi(\ulcorner\sigma\urcorner)$} \} $. I don't know how to formalize this in $\text{PA}$, let alone prove something about it.


*The same thing with the talk about models of $T$. Say $T = \text{ZFC}$, then how can you even state in the language of arithmetic that there is a model of $T$ with such and such property (its elementary diagram is the above set and its universe)?


*A different type of question: what is the use of this theorem (in general terms, beyond the mentioned paper)? Why is it called the arithmetized completeness theorem?
 A: Re: $(1)$, there's less here than meets the eye. The key point is that we can whip up a formula $\theta$ which defines the set of Godel numbers of $\overline{\mathcal{L}}$-sentences; with this in hand, we're just looking at $$S=\{x: \theta(x)\wedge\phi(x)\}.$$ This is pretty boringly definable.
Now when we say that $S$ is the elementary diagram of some structure with domain $C$, we mean that $S$ satisfies the usual properties of an elementary diagram - and since these are syntactic properties, we can via Godel numbering express that $S$ does or does not have them. For example, we'll want each of the following:

*

*If $\ulcorner\sigma_0\urcorner$, $\ulcorner\sigma_1\urcorner\in S$ then $\ulcorner\sigma_0\wedge\sigma_1\urcorner\in S$.


*If $\ulcorner \exists x\sigma(x)\urcorner\in S$ then for some $c\in C$ we have $\ulcorner\sigma(c)\urcorner\in S$. (This addresses the "with universe from $C$" bit.)


*$\ulcorner\perp\urcorner\not\in S$.
A bit more accurately, we have primitive recursive functions corresponding to e.g. conjunction and to existential quantification with respect to some fixed variable, and the first two bulletpoints above amount to appropriate closure/existence conditions on $S$ with respect to these functions. The third bulletpoint meanwhile prevents triviality.
Basically, the point is that the property of being the elementary diagram of some structure with domain $\mathbb{N}$ is first-order expressible (because it amounts to "local closure/existence/nonexistence conditions" per the above).

Re: $(2)$, intuitively speaking the point is that we're not talking about arbitrary models of e.g. $\mathsf{ZFC}$, but only the ones with domain $\mathbb{N}$. A structure with domain $\mathbb{N}$ is entirely described by a single set of natural numbers $X$, and "$X$ is the atomic diagram of a model of $\mathsf{ZFC}$" is per the above first-order expressible: we just say "$X$ has the basic syntactic properties above, and each $\mathsf{ZFC}$-axioms is in $X$."
I think this might be made more mysterious because we usually think of models of $\mathsf{ZFC}$ as being highly complicated and definitely not having domain $\mathbb{N}$. But per downwards Lowenheim-Skolem, $\mathsf{ZFC}$ (assuming it's consistent at all) also has lots of models with domain $\mathbb{N}$. These are the models which we're able to consider in this approach.

Re: $(3)$, the point is that the usual phrasing of the completeness theorem

every consistent theory has a model

is totally bonkers in the context of arithmetic. Basically, we can only directly talk about finite sets in the language of arithmetic, so if we naively "arithmetically phrase" the sentence "Presburger arithmetic has no models" we get something true.
(See for example the Ackermann interpretation. We can pass from (say) $\mathsf{PA}$ to an appropriately-equivalent theory of sets, but that theory proves "Every set is finite.")
So if we want some version of the completeness theorem to hold in a theory of arithmetic, its "models" have to consist of relations on the whole universe; and of course they'll have to consist of definable relations, since we can't talk about undefinable relations internally.
Another option would be to use conservative extensions which can talk about infinite sets directly; this is for example the approach taken here. In all the contexts I've played with this approach works and so I generally prefer it. That said, $(i)$ if I recall correctly there are situations where this approach is either annoyingly nasty or obscures valuable information (I think this occurs with very weak theories of arithmetic) and $(ii)$ the fact that we can get a completeness theorem just in the language of first-order arithmetic is interesting on its own.
