Timeline for Does "every" first-order theory have a finitely axiomatizable conservative extension?
Current License: CC BY-SA 4.0
13 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Dec 2, 2019 at 12:27 | vote | accept | Oscar Cunningham | ||
Mar 27, 2019 at 15:25 | comment | added | James E Hanson | @OscarCunningham It's perfectly possible to write down a sentence in, say, $\sf ZFC$ that means $M \models T$ for a non-c.e. theory $T$, but the problem is that in a non-standard model of our extension can be wrong about what $T$ is in a 'harmful' way. If $T$ is c.e. the extension might enumerate incorrect standard axioms into $T$, but it's still true that $M$ models the 'real' $T$ since it's satisfying more axioms. On the other hand if $T$ is co-c.e., for instance, then a non-standard model might remove axioms from $T$, so the internal model of $T$ may fail to be an external model of $T$. | |
Mar 27, 2019 at 15:09 | history | became hot network question | |||
Mar 27, 2019 at 14:58 | answer | added | Emil Jeřábek | timeline score: 29 | |
Mar 27, 2019 at 14:40 | comment | added | François G. Dorais | (Actually, it is essential because having a conservative finitely axiomatizable extension means that you must be recursively axiomatizable.) | |
Mar 27, 2019 at 14:39 | comment | added | François G. Dorais | That's probably not completely essential but otherwise you have to come up with a way to say "$M \vDash T$" in one sentence. | |
Mar 27, 2019 at 13:41 | comment | added | Oscar Cunningham | @FrançoisG.Dorais Why does this only work for effectively axiomatizable theories? | |
Mar 27, 2019 at 12:16 | comment | added | François G. Dorais | [...] The reason why this works is that "conservativity" depends on how the theory is interpreted in the larger one. In this case, the interpretation is through the new constant $M$. Note that if, for example, the theory $T$ is $PA$, for example, the interpretation does not use the natural interpretation of natural numbers in the larger theory. Even if the larger theory proves $\operatorname{Con}(T)$ there is no reason for $M \vDash \operatorname{Con}(T)$ to be true. This is probably not what Oscar really wants... | |
Mar 27, 2019 at 12:13 | comment | added | François G. Dorais | @JamesHanson is right but there is an issue with what "conservativity" means, which I think is not what the OP is intending. Pick a strong enough finitely axiomatizable theory, say NGB, which is reasonably sound for arithmetic, that can make sense of the model theoretic satisfaction relation. If $T$ is recursively axiomatizable, then add a constant $M$ and an axiom that says $M \vDash T$ where $\vDash$ and $T$ are interpreted in their natural way in the larger theory. [...] | |
Mar 27, 2019 at 11:53 | history | edited | Oscar Cunningham | CC BY-SA 4.0 |
deleted 2 characters in body
|
Mar 27, 2019 at 11:31 | comment | added | James E Hanson | The part I'm sketchiest on is the finite axiomatizability, but I think you can add classes like in $\sf NGB$ to get a finitely axiomatizable theory. | |
Mar 27, 2019 at 11:28 | comment | added | James E Hanson | I suspect the answer is yes via some modified form of $\sf KPU$ that is finitely axiomatizable. Basically the idea is that once you add superstructure that is strong enough to formalize computability it can say that the sort of urelements is a model of the original theory in a single sentence. You can show conservativity by showing that every model of the original theory extends to a model of the new theory. | |
Mar 27, 2019 at 11:09 | history | asked | Oscar Cunningham | CC BY-SA 4.0 |