For two theories $T,T'$, what does $T\vdash Con(T')$ really tell us about the models of $T$?

Question

Inspired by this question, which I realized I couldn't answer (because model theory and me don't get along).

I've made a few edits to (hopefully constructively) tighten the question a bit.

If for theories $T,T'$ it happens that $T\vdash Con(T')$, what does this really tell me about models of $T$ with respect to $T'$? Does it tell us that every model of $T$ has a definable substructure that's a model of $T'$, or is it more subtle? Or is it even interesting from a model theoretic standpoint (i.e. is the proof theoretic relationship between $T$ and $T'$ generally the only interesting one)?

I would like to assume $T$ and $T'$ can both yield PA by default, but I would be interested if anything general can be said about weaker theories.

Answer 1

It is not literally true that if $T \vdash \operatorname{Con}(T')$ then every model of $T$ has a definable substructure that satisfies $T'$. For example, $T'$ might not even be in the same language as $T$, in which case no substructure of a model of $T$ can possibly satisfy $T'$.

For example, PA proves the consistency of a theory of second-order arithmetic known as $\mathsf{RCA}_0$. Now the language for $\mathsf{RCA}_0$ includes a relation symbol $\in$ that is not in the language of PA, so no substructure of PA can satisfy $\mathsf{RCA}_0$.

Similarly, PA + Con(ZFC) proves Con(ZFC), but no model of PA has a substructure that satisfies ZFC.

It is true, however, that every model of PA intereprts a model of $\mathsf{RCA}_0$. But every model of PA interprets a stronger theory of second-order arithmetic, $\mathsf{ACA}_0$, which is equiconsistent with PA. So it is also not true that $T \vdash \operatorname{Con}(T')$ is equivalent to saying that $T$ interprets $T'$.

If every model of $T$ has a definable substructure satisfying $T'$ (or, in fact, any substructure satisfying $T'$), that only shows that Con($T$) implies Con($T'$).

Answer 2

Suppose $T$ and $T'$ are both theories in the language of first-order arithmetic $\mathscr L_{\mathrm{A}}$, and $T\vdash\mathrm{Con}(T')$. (This presumes the fact that $T'$ is definable in $\mathscr L_{\mathrm{A}}$.) If $T$ is strong enough to prove an appropriate version of Gödel's Completeness Theorem (in the sense described in my comment below), then, as you wrote, for every model $M\models T$, there is $K\models T'$ that is definable in $M$ (and so we may regards $K\subseteq M$).

For me, it is actually more interesting to consider this $K$ as an end-extension of $M$ (provided $T'$ extends, say, $\mathrm{PA}^-$). One can do this because in the $M$-version of $\mathscr L_{\mathrm A}$, there is a closed term $$ 0+\underbrace{1+1+\cdots+1}_{\text{$m$ $1$'s}} $$ for every $m\in M$. As $K\models\mathrm{PA}^-$, the realizations of these terms form an initial segment of $K$, which we can identify with $M$. This is interesting because many important problems in the area are related to end-extensions.