Timeline for Are there any natural recursively but not primitive-recursively axiomatized theories?
Current License: CC BY-SA 3.0
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 5, 2012 at 18:18 | comment | added | Ali Enayat | Emil: we are on the same page; in light of undecidability result you mention, a more hopeful option is to replace + with the successor function in my proposed structure. | |
| Jul 5, 2012 at 11:39 | comment | added | Emil Jeřábek | In principle, pairing by itself does not imply undecidability, that’s why I only expressed a doubt. However, it does make it very suspect, as naturally occurring theories with pairing are usually undecidable. Notice also that Cantor’s pairing function is undecidable in the presence of addition. | |
| Jul 4, 2012 at 19:12 | comment | added | Ali Enayat | Emil, the theory of Cantor's pairing function is decidable, so that by itself should not be problematic (the result is due to Cegielski & Richard, 1999). | |
| Jul 4, 2012 at 17:40 | comment | added | Emil Jeřábek | Also, I rather doubt the first-order theory of $(\mathbb N,0,1,+,f_G)$ could be decidable, since something like $f_G(x+y)+x$ should give a pairing function. | |
| Jul 4, 2012 at 17:32 | history | edited | Ali Enayat | CC BY-SA 3.0 |
added 111 characters in body
|
| Jul 4, 2012 at 16:34 | comment | added | Emil Jeřábek | I mean, injective unary function with an infinite $f$-chain (or arbitrarily large cycles). | |
| Jul 4, 2012 at 16:24 | comment | added | Emil Jeřábek | The equational theory of $f_G$ is the same as the equational theory of any other injective unary function: no two syntactically distinct terms are equal. Presumably Ali meant the equational theory of $(\mathbb N,0,S,f_G)$, whose complexity is rather unclear to me: the obvious argument why it shouldn’t be primitive recursive fails as $f_G$ has indeed prim rec graph, but on the other hand, I don’t see how to check equality of more complex terms by a prim rec algorithm (though I’d be inclined to conjecture this is possible). | |
| Jul 4, 2012 at 16:06 | comment | added | Joel David Hamkins | Ali, isn't the equational theory of your Goodstein example still primitive recursive? (But actually, I not precisely sure exactly what you mean) But the question of whether $f(m)=n$ is a primitivie recursive relation in both $m$ and $n$, since given $m$ and $n$ I can by a primitive recursive function run the Goodstein construction on $m$ for $n$ steps and see if I get $0$ or not. | |
| Jul 4, 2012 at 15:28 | comment | added | Ali Enayat | Emil, thanks for your comments. I have completely changed my PS in light of your remarks. I have suggested a possible "dream solution" to the question posed at the end of your comment. | |
| Jul 4, 2012 at 15:26 | history | edited | Ali Enayat | CC BY-SA 3.0 |
deleted 139 characters in body
|
| Jul 4, 2012 at 12:21 | comment | added | Emil Jeřábek | I’m afraid I don’t understand the point of the PS. First, the natural axiomatization of $\overline T$ is the same as the natural axiomatization of $T$, which is of very low complexity for the examples you mention. Second, the deductive closure itself is primitive recursive for all your examples. In fact, this could be an interesting variant on Peter’s question: are there any natural examples of decidable deductively closed theories that are not primitive recursive? | |
| Jul 4, 2012 at 3:00 | history | edited | Ali Enayat | CC BY-SA 3.0 |
added 782 characters in body
|
| Jul 4, 2012 at 1:49 | comment | added | Ali Enayat | I think what made Joel and I reach for our r.e.(c.e) examples is that Craig's trick works equally well for r.e. sets and recursive sets of axioms. I will add a PS to offer an example that might be of the sort you are looking for. | |
| Jul 3, 2012 at 23:14 | comment | added | Peter Smith | Yep my hope is that there's little mathematics at stake. But I was a bit worried I was missing something interesting ....! | |
| Jul 3, 2012 at 19:55 | comment | added | Joel David Hamkins | What we gave were examples of theories whose natural axiomatization is c.e. rather than decidable. But you want an analogous example separating decidable from primitive recursive... | |
| Jul 3, 2012 at 19:13 | comment | added | Joel David Hamkins | Well, I agree, and it's back to the drawing board for both of us! At the same time, one might object that the question has little mathematics at stake, but rather only the interpretation of what counts as sufficiently "natural". | |
| Jul 3, 2012 at 18:25 | comment | added | Peter Smith | [Sorry for the seemingly unappreciative terseness, due to the constraints of the comment box!] | |
| Jul 3, 2012 at 18:24 | comment | added | Peter Smith | A lovely example, of course! But what exactly it is an example of? $T_{ZFC}$ is, as you say, a natural r.e. set of sentences of great interest. But it isn't, as presented, a recursively axiomatized theory in the sense in my question -- taking those sentences as the axioms, the property-of-numbering-an-axiom (i.e. of numbering an arithmetical consequence on ZFC) isn't recursive. And the nice reaxiomatizations are primitively recursively axiomatized, no? So the question remains doesn't it? Are there natural cases of decidable axiomatized theories, where the decision requires unbounded search? | |
| Jun 30, 2012 at 22:37 | vote | accept | Peter Smith | ||
| Jun 30, 2012 at 22:38 | |||||
| Jun 30, 2012 at 19:28 | comment | added | Joel David Hamkins | Excellent example, Ali. Another similar example would just be the theory TA of true arithmetic. This is a commonly considered theory, but of course is not computably or even arithmetically axiomatizable. I would encourage Peter to accept your answer instead of mine...(or wait for even more examples!) | |
| Jun 30, 2012 at 14:31 | history | answered | Ali Enayat | CC BY-SA 3.0 |