Timeline for An element $g$ in a group such that neither $g=1$ nor $g\ne 1$ can be proved.
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 17, 2013 at 17:49 | history | edited | Benjamin Steinberg | CC BY-SA 3.0 |
added 151 characters in body
|
| Feb 17, 2013 at 17:45 | comment | added | Benjamin Steinberg | @Joel, not being a logician I didn't know the difference between a Gödel statement and a Rosser one. Thanks for the correction. | |
| Feb 17, 2013 at 17:43 | comment | added | Benjamin Steinberg | Joel, I think non-Higman proofs work just as well but Higman proofs are easier to write down (modulo the Higman theory). @aglearner, Higman embeddings are explicit/effective so you get an explicit group and element | |
| Feb 17, 2013 at 17:13 | comment | added | Joel David Hamkins | Benjamin, can't you avoid the Higman embedding theorem by using the usual idea that embeds Turing machines into group presentations? That is, for each Turing machine $M$ there is a finite group presentation and a generate $g$ such that $g=1$ in the presentation if and only if $M$ halts. Since for any given background theory $T$, there are explicit Turing machines $M$ for which $T$ neither proves nor refutes whether $M$ halts, we get explicit finite group presentations such that whether $g=1$ or not is not provable in $T$. | |
| Feb 17, 2013 at 16:57 | comment | added | aglearner | Benjamin, just to make sure, such a group will be finitely presented with an explicit presentation and there will be an explicit element $g$ in it? I have to apologize, my knowledge of logics is close to $0$. | |
| Feb 17, 2013 at 16:56 | comment | added | Joel David Hamkins | Yes, and one can use any statement that is independent of the background theory. To use the Godel sentence, as here, one needs to make a slightly stronger meta-theoretic assumption on the background theory, whereas if one uses the Rosser sentence instead, it goes through just with the assumption that the background theory is consistent. | |
| Feb 17, 2013 at 16:53 | comment | added | Benjamin Steinberg | I'm assuming finite proof is defined and a finite proof of the group theory fact can be then unwound to the arithmetic one. | |
| Feb 17, 2013 at 16:46 | history | answered | Benjamin Steinberg | CC BY-SA 3.0 |