Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
up vote 1 down vote accepted

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'$).

share|cite|improve this answer
Excellent! You've given an example where $PA$ interprets $ACA_0$ and can't yield $Con(ACA_0)$; are there examples of the converse? E.g. is it also the case that $PA+Con(ZFC)$ can't interpret $ZFC$? This sounds plausible, but I distrust plausible-sounding things... – Malice Vidrine Nov 16 '13 at 16:02
@Carl: The parenthetical remark in your last paragraph looks suspicious. For example, every model of $\mathrm{PA}$ has an initial segment isomorphic to $\mathbb N$. However, this doesn't mean that $\mathrm{Con(PA)}$ implies $\mathrm{Con}(T)$ (say, over $\mathrm{PA}$) for every true recursive theory $T$. – Lawrence Wong Nov 16 '13 at 17:13
@Lawrence Wong: it does imply that; the key issue is to remember the metatheory where the result is proved. I mean that if $M$ is a sufficiently strong metatheory (e.g. ZFC) and $M$ proves that every model of $T$ has a substructure satisfying $T'$, then $M$ also proves that Con($T$) implies Con($T'$). Of course this can happen even if $M$ does not already prove Con($T$); for example ZFC proves that the consistency of ZFC plus a measurable cardinal implies the consistency of ZFC plus an inaccessible cardinal, but it does not prove either consistency statement on its own. – Carl Mummert Nov 16 '13 at 18:43
@Malice Vidrine: the closest thing I see to that is the comment by Lawrence Wong below his answer. You could ask the question in your comment as a separate question, I think it is quite interesting. – Carl Mummert Nov 16 '13 at 18:46
@Carl Mummert: You were right. Now, I see why I was confused. Of course "$\mathrm{PA}\vdash\mathrm{Con(PA)}\rightarrow\mathrm{Con}(T)$ for every recursive theory $T$ true in $\mathbb N$" is wrong. My argument only showed that if we replace the base theory $\mathrm{PA}$ by a theory $S$ good enough to talk about natural number arithmetic, and suppose $S$ thinks its natural numbers satisfy $T$, then $S\vdash\mathrm{Con(PA)}\rightarrow\mathrm{Con}(T)$. This has (almost) nothing to do with the real $\mathbb N$ (and actually tells us nothing). It is much clearer to me now. Thank you very much! – Lawrence Wong Nov 17 '13 at 9:51

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.

share|cite|improve this answer
Could you clarify the form of the completeness theorem that is provable in PA? – Carl Mummert Nov 16 '13 at 14:13
@Carl Mummert: This is the same as what you have in $\mathrm{WKL_0}$; so strictly speaking, it is not expressible in the language of first-order arithmetic. To put it model-theoretically: if $M\models\mathrm{PA}$ and $T'$ is a theory definable in $M$ such that $M\models\mathrm{Con}(T')$, then there is a model of $T'$ definable in $M$. – Lawrence Wong Nov 16 '13 at 16:51
!Lawrence Wong: thank you, that is completely clear. – Carl Mummert Nov 16 '13 at 18:47

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.