MathOverflow is a question and answer site for professional mathematicians. 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

What I mean is this. By downward Lowenheim-Skolem theorem, first-order formula Q is a always true iff it is true in every countable structure. But is there some first-order formula Q which is true in every computable structure and false in some non-computable structure? My feeling is that of course the answer should be "yes", but I can't construct an example. I feel also that the questions of the sort has been widely studied. (For example, maybe some study of conditions under which first-order theory has computable model or hasn't). Do you know anything about that?

Thanks in advance.

share|cite|improve this question
MO points out… as related. Does this already answer your question? – Carsten S Aug 2 '10 at 11:12
Thanks, it partially answers. ZFC is infinite theory, but what about one sentence? – Sergei Tropanets Aug 2 '10 at 12:07
As Carl Mummert points out in the answer below the first part of a question is <<about all countable models in the language of particular formula, rather than all models of a particular theory.>> So, more generally, is there a first-order theory which is true in all computable structures and false in some (all) uncomputable? Can it be finite or infinite? – Sergei Tropanets Aug 2 '10 at 12:24
I think I answered this in the question below. If I didn't, could you clarify the question? – Carl Mummert Aug 2 '10 at 15:57
up vote 8 down vote accepted

There is no computable, countable nonstandard model of Peano arithmetic. This result is known as Tennenbaum's theorem after Stanley Tennenbaum. There is an online paper at [1]. So if you take any sentence $R$ in the language of PA that is not true in the standard model but is consistent with PA, it will be true in some countable model of PA but not in the (unique, up to isomorphism) computable model of PA.

But I'm not sure if that addresses your question, because that answer is about models of a theory. In your question, it seems like you're talking about all countable models in the language of particular formula, rather than all models of a particular theory.

To make the answer fit that question, we want to replace PA with a finitely axiomatized subtheory of PA for which the only computable model is the standard model. There is a heuristic principle that we should be able to find a subtheory like this by examining the proof of Tennenbaum's theorem, and reference [1] confirms that this does work.

Let $T$ be the sentence that is the conjunction of the axioms of this subtheory. Let $R$ be the independent sentence from the first part, and look at the sentence $T \rightarrow \lnot R$. This will be true in every computable model (because the only computable model that satisfies $T$ is the standard model, which satisfies $\lnot R$). It will be false in any countable nonstandard model of PA in which $R$ holds, because $T$ is a subtheory of PA.

1: Richard Kaye, "Tennenbaum's Theorem for Models of Arithmetic",

(Note: I corrected the last paragraph based on a comment by Sergei Tropanets.)

share|cite|improve this answer
<<Let R be the independent sentence from the first part>>, you mean of course negation of R. <<There is a heuristic principle that we should be able to find a subtheory like this by examining the proof of Tennenbaum's theorem>> I'll check that. Thank you! But can you just outline the idea? – Sergei Tropanets Aug 2 '10 at 14:30
The idea is that most proofs like the proof of Tennenbaum's theorem only refer to some finite number of axioms of the theory in question. So by examining the proof, you can make a list of all the axioms that are actually required, and then take that list as your finite subtheory. This idea may not work for every single proof, but it works for many proofs in practice. For example, it applies to the proof of Goedel's first incompleteness theorem, where Robinson arithmetic is (essentially) the finite list of axioms you obtain by examining which axioms of PA are actually required in the proof. – Carl Mummert Aug 2 '10 at 15:44
Yes, you answered the question, though for me personally it will be necessary to analyze that proof and to actually extract the finite subtheory. But one natural additional question arises: can the class of all computable structures be characterized by first order theory, i. e., is there some first-order theory T which is true in all computable structures and false in all uncomputable? Another one: ZFC and similar systems don't have computable models because of their strength which allows them to "construct non-standard models of PA", but what about weaker theories? Thanks very much again! – Sergei Tropanets Aug 2 '10 at 16:58
There's an issue with signatures: your first-order theory would have some signature, but an arbitrary computable structure could have some other signature. In general, the questions here are heading towards computable model theory; there's a survey article about that in the Handbook of Computability Theory. The general question of when a theory has a computable model is not settled AFAIK; see that article for more info. There's not much room in these comments to try to answer all the follow-up questions, though. You could try asking them as a new MO question (or multiple questions). – Carl Mummert Aug 2 '10 at 18:14
@Sergei: The property of being (isomorphic to) a computable structure is not preserved under elementary equivalence, hence no such theory $T$ can exist, even in a fixed language. For example, $M=(\mathbb N,+)$ is computable, but for every $X\subseteq\mathbb N$, there exists a countable elementary extension $M'$ of $M$ and $a\in M'$ such that $X=\{n\in\mathbb N:M'\models p_n∣a\}$, where $p_n$ denotes the $n$th prime. This makes both $X$ and its complement existentially definable in $M'$ (with parameter $a$), hence if $X$ is not computable, $M'$ cannot be computable either. – Emil Jeřábek Nov 5 '12 at 16:21

Carl's answer is correct.

There is also a to more direct way to achieve the same thing. The Tennenbaum's theorem holds for much weaker theories, e.g. $I\Delta_0$ (even for far weaker theories like $IOpen$ plus some number theoretic principles, but not for $IOpen$, a result due to Shepherdson).
$I\Delta_0+exp$ is finitely axiomatizable, see Haim Gaifman and Constantine Dimitracopoulos, "Fragments of Peano's Arithmetic and the MRDP Theorem". It is also a sub-theory of $PA$.

For more on Tennenbaum's theorem and weak arithmetics, have a look at this paper:
Shahram Mohsenipour, "Hierarchies of Subsystems of Weak Arithmetic", to appear
in "Set theory, Arithmetic, Philosophy: Essays in Memory of Stanley Tennenbaum" (edited by J. Kennedy and R. Kossak), Cambridge University Press.

share|cite|improve this answer

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.