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 22, 2013 at 17:25 | vote | accept | aglearner | ||
| Feb 17, 2013 at 20:42 | comment | added | Benjamin Steinberg | Basically a yes to the original question automatically builds a yes to the second because the unprovable thing must be in the no part. | |
| Feb 17, 2013 at 20:41 | comment | added | Benjamin Steinberg | Ok I understand now. In your construction the Turing machine simply does not halt. But you cannot write a proof it does not halt in the theory T. Also I now understand what you mean by the original question is equivalent to the adjusted one. Thanks. | |
| Feb 17, 2013 at 20:24 | comment | added | Joel David Hamkins | That said, I'm not clear on what the difference is with the "adjusted" question, since proofs are finite objects anyway, so they all take "finite time". Part of the confusion may be that the OP was not clear about what theory it is in which we are to find the proofs. In particular, one can think about Mark's proof that $g\neq 1$ was made under the assumption $\phi$ that there is no proof of $g=1$ (in the base theory $T$), and so it is not a proof in $T$, but a proof in $T+\phi$. | |
| Feb 17, 2013 at 20:18 | comment | added | Joel David Hamkins | The claim that if $g=1$, then this is provable, is entirely fine, and that was what Mark argued. We all agree with that. My point is that this doesn't imply that there can't be a group presentation with a word $g$ for which our theory is unable to prove or refute $g=1$. Thus, for any such presentation, either $g=1$ is provable or $g\neq 1$ is true (but perhaps not provable). This is exactly the same as with Turing machines: if a machine does halt, this is provable even in very weak theories. But meanwhile, there are still some machines such that we cannot prove or refute whether they halt. | |
| Feb 17, 2013 at 20:02 | comment | added | Benjamin Steinberg | @Joel, I still don't quite understand why Mark's answer to the original question is wrong and yours works for the original question (as opposed to the adjusted one). It seems to me that no matter the background theory if M is a Turing machine and M halts on the empty string then there is a finite proof, namely the halting computation. It seems to me that one can only not be able to produce a finite proof that it doesn't halt. | |
| Feb 17, 2013 at 18:43 | comment | added | aglearner | Joel, thank you for this detailed answer! (I will need some time to understand it) | |
| Feb 17, 2013 at 17:27 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |