Timeline for Does "every" first-order theory have a finitely axiomatizable conservative extension?
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 15, 2020 at 7:27 | history | edited | CommunityBot |
Commonmark migration
|
|
| Dec 2, 2019 at 12:27 | vote | accept | Oscar Cunningham | ||
| Dec 2, 2019 at 12:17 | comment | added | Emil Jeřábek | @OscarCunningham There is more than one way how to show this, but for example it follows immediately from the above mentioned result that any r.e. theory with only infinite models has a finite conservative extension: simply endow the given theory with a new sort (with no further structure), and axioms that make it infinite. (Or, to present it differently, relativize the original theory to a new unary predicate, and include axioms that make the domain infinite.) Then apply the original result. | |
| Dec 2, 2019 at 11:47 | comment | added | Oscar Cunningham | @EmilJeřábeksupportsMonica Sorry for taking a while to get back to this. Where would I look for a proof of "If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension."? | |
| Mar 29, 2019 at 18:34 | comment | added | Fedor Pakhomov | @EmilJeřábek Yes, it would be good to give this problem a try. | |
| Mar 29, 2019 at 15:04 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
added 64 characters in body
|
| Mar 29, 2019 at 15:01 | comment | added | Emil Jeřábek | It seems I didn’t think it through, I underestimated the issues that arise. Thank you both for pointing it out. I’ll stick to facts rather than vague ideas for now. @Fedor That’s an interesting paper, I didn’t know you did some work on this. Maybe we could have a look at the problem after you arrive. | |
| Mar 29, 2019 at 14:56 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
the proof outline is not correct, as pointed out in comments
|
| Mar 29, 2019 at 6:24 | comment | added | Fedor Pakhomov | Although I don't see how to properly axiomatize a truth predicate, when you use $\mathsf{PA}^{\mathsf{top}}$ as the theory of numbers. The issue is that even in the situation when the model $M\models \mathsf{PA}^{\mathsf{top}}$ is infinite and $\varphi(x)$ is some standard formula, within $M$ we wouldn't have Gödel numbers for all the substitutions $\varphi[a/x]$, for $a\in M$. Using this behavior, for example, one could easily define a truth predicate $\top$ that satisfy the compositional axioms in an infinite $M$, but wouldn't agree with the external truth definition on standard sentences. | |
| Mar 29, 2019 at 5:51 | comment | added | Fedor Pakhomov | It is cool: actually in a recent paper by A. Visser and me "On a question of Krajewski's" arxiv.org/pdf/1712.01713.pdf, we considered the second theorem from your answer to be an open problem (Open Question 3.4). | |
| Mar 28, 2019 at 16:33 | comment | added | Dmytro Taranovsky | This works for axiom schemas with $O(1)$ different variable symbols (which would be achievable if we had pairing), but the issue I see is that in general (under plausible computational complexity assumptions) every $Σ^1_1$ statement will have a limit on the number of universally quantified variables it can handle in the truth predicate. | |
| Mar 28, 2019 at 13:48 | comment | added | Emil Jeřábek | I believe one can actually do that, see the update. | |
| Mar 28, 2019 at 13:47 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
expand
|
| Mar 27, 2019 at 17:09 | comment | added | Emil Jeřábek | ... about infinite models of $\Phi$, and it is not clear to me that we can combine $\Phi$ and $\Psi$ to a formula that works for all models. Perhaps one can extract something like this from the construction of $\Phi$ or $\Psi$, but this is not a priori obvious. | |
| Mar 27, 2019 at 17:07 | comment | added | Emil Jeřábek | Yes, for finite models, being in NP is the same as being $\Sigma^1_1$-definable. However, what is unclear to me is the following. Assume that $T$ is a r.e. theory whose finite models are NP. Then, there is a $\Sigma^1_1$ sentence $\Phi$ such that $M\models T\iff M\models\Phi$ for finite models $M$. By the results above, there is also a $\Sigma^1_1$ sentence $\Psi$ such that $M\models T\iff M\models\Psi$ for infinite models $M$. We may actually assume that $\Psi$ has no finite models, as infiniteness is $\Sigma^1_1$. However, finiteness is not $\Sigma^1_1$, hence we have no information ... | |
| Mar 27, 2019 at 16:45 | comment | added | Dmytro Taranovsky | Sorry for the mistake. To complement your comment, for finite models (in logic with identity and finitely many symbols), "equivalent to a $Σ^1_1$ second-order sentence" is the same as being in NP. This condition holds for typical but not all theories, and is not needed if we are permitted to expand the universe with new types. | |
| Mar 27, 2019 at 16:15 | comment | added | Emil Jeřábek | @DmytroTaranovsky That does not sound right. Testing whether a given finite model expands to a model of a specific finite theory can be done in NP, hence a necessary condition is that finite models of the theory can be recognized in NP, not just in PH. In fact, a necessary and sufficient condition is that the theory is equivalent to a $\Sigma^1_1$ second-order sentence, but this is really just a trivial restatement of the definition, if you think about it. | |
| Mar 27, 2019 at 14:58 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |