I'm wondering what results are typically used to show that a first-order logic theory captures its intended meaning.
To make things concrete, suppose I have a signature $\Sigma = \{ 0, S, =, +, \leq \}$ and I define a theory T that tries to capture the expected meaning of these symbols (something like Peano's axioms). How to state formally it is indeed the case?
I'm thinking of something along these lines: "For all formulas $P$, we have $T \vDash_1 P$ if and only if $ \vDash_2 P$", where $\vDash_1$ is the usual entailment relation with the signature symbols uninterpreted, and $\vDash_2$ gives them their "meta-level" meaning. Is that correct?