Timeline for Are computable models sufficient?
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 5, 2012 at 16:21 | comment | added | Emil Jeřábek | @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. | |
| Aug 2, 2010 at 18:14 | comment | added | Carl Mummert | 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). | |
| Aug 2, 2010 at 16:59 | vote | accept | Sergei Tropanets | ||
| Aug 2, 2010 at 16:58 | comment | added | Sergei Tropanets | 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! | |
| Aug 2, 2010 at 15:48 | history | edited | Carl Mummert | CC BY-SA 2.5 |
Correct last paragraph
|
| Aug 2, 2010 at 15:44 | comment | added | Carl Mummert | 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. | |
| Aug 2, 2010 at 14:30 | comment | added | Sergei Tropanets | <<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? | |
| Aug 2, 2010 at 11:51 | history | answered | Carl Mummert | CC BY-SA 2.5 |