Timeline for Uniform solutions to Post's problem for axiomatizable theories
Current License: CC BY-SA 2.5
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 8, 2012 at 11:24 | comment | added | Emil Jeřábek | Not only can Rosser’s sentence depend on the enumeration, but in fact, it can also depend on the method of diagonalization. That is, there exist proof predicates for which Rosser’s fixed point equation has more than one solution up to provable equivalence. This is an old result of (IIRC) Guaspari and Solovay. (In contrast, Gödel’s sentence, and more generally any fixed point equation using just the provability predicate and Boolean connectives, is unique up to provable equivalence, for a fixed proof predicate.) | |
| May 30, 2010 at 21:58 | comment | added | François G. Dorais | Why is it necessary to prove the equivalence internally? | |
| May 30, 2010 at 21:45 | comment | added | Joel David Hamkins | I doubt it. At the very least, it would seem required for the theory to prove that the enumerations gave the same theory, not merely that this was true. | |
| May 30, 2010 at 21:30 | comment | added | François G. Dorais | I don't know if Rosser's sentence gives a theory which is independent of the enumeration of T. Do you happen to know? | |
| May 30, 2010 at 20:51 | comment | added | François G. Dorais | I wasn't assuming that $T'$ is consistent; the inconsistent theory is the top of the lattice. However, you are right that using Rosser's sentence instead is perfectly justifiable. | |
| May 30, 2010 at 20:47 | history | edited | Joel David Hamkins | CC BY-SA 2.5 |
deleted 20 characters in body
|
| May 30, 2010 at 20:33 | history | answered | Joel David Hamkins | CC BY-SA 2.5 |