Timeline for Element being trivial in a finitely presented group independent of ZFC
Current License: CC BY-SA 4.0
22 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 30, 2021 at 15:12 | vote | accept | CommunityBot | ||
| Apr 22, 2021 at 8:29 | comment | added | HJRW | ... (cont'd) For a specific example of a group, presumably any "universal" finitely presented group (i.e. one into which all other fp groups embed) would suffice? The one given in this paper -- arxiv.org/abs/1610.00977 -- maybe the smallest known, with 8 generators and 26 relations. I'm uncertain how you would find the explicit element, though... | |
| Apr 22, 2021 at 8:28 | comment | added | HJRW | @MaximeRamzi, the actual construction of groups with unsolvable word problem is complicated, but if you want to understand the idea I suggest you first look up the Higman Embedding Theorem (en.wikipedia.org/wiki/Higman%27s_embedding_theorem). It's relatively easy to write down a recursively presented group with unsolvable word problem, and then the HET produces a finitely presented example. | |
| Apr 22, 2021 at 6:57 | comment | added | Joel David Hamkins | In this paper arxiv.org/abs/1605.04343, the authors provide a 7910-state Turing machine whose behavior is independent of ZFC. I think most people think the true bound is considerably less, but proving this is finicky. | |
| Apr 22, 2021 at 6:45 | comment | added | user178109 | I was curious if say there is a such a group and an element that can be written down in 1 kilobyte or less. Though this is still informative! | |
| Apr 21, 2021 at 21:18 | comment | added | Joel David Hamkins | Oh, I think there are some nice accounts of that part. Perhaps the combinatorial group theory people can post a link to the most accessible source for showing the word problem is undecidable. | |
| Apr 21, 2021 at 21:16 | comment | added | Maxime Ramzi | Yeah, I guessed that, but I meant a sketch of how one encodes a halting problem in a word problem. But maybe the answer is the same here | |
| Apr 21, 2021 at 21:07 | comment | added | Joel David Hamkins | @MaximeRamzi Providing the actual group presentation will be extremely detailed and finicky, since it will involve implementing all the encoding of the halting problem of that rather complicated program into the word problem. I'm not sure if this has ever actually been done in practice. So this is a pure-existence proof of an explicit object, which I fully admit may not be seen as satisfactory except in theory. | |
| Apr 21, 2021 at 21:07 | comment | added | Burak | @HJRW: You may be interested in the following answer, which -not surprisingly- is again by Joel. mathoverflow.net/a/27677/33039 Suppose that you prove in $ZFC$ that a $\Pi_1$-sentence $\varphi$ (such as "the Turing machine blah blah does not halt") is independent of $ZFC$. In particular, you can prove in $ZFC$ that $Con(ZFC) \rightarrow Con(ZFC+\varphi)$. Then you can prove $\varphi$ from $ZFC+Con(ZFC)$, but not $ZFC$ alone. So this does not contradict that it is independent of $ZFC$. | |
| Apr 21, 2021 at 21:05 | comment | added | Maxime Ramzi | Having never seen the construction, I don't know if that's reasonable, but it could be nice to sketch a construction of $G$ and/or link to a reference where this is explicitly done. But nice answer either way ! | |
| Apr 21, 2021 at 21:03 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 72 characters in body
|
| Apr 21, 2021 at 20:56 | comment | added | Joel David Hamkins | The general fact used in my answer is that every true existential arithmetic statement is provable in PA and ZFC. So if such a statement is independent, it must not be true. But there are models going both ways, and that is what independence amounts to. | |
| Apr 21, 2021 at 20:53 | comment | added | HJRW | @JoelDavidHamkins: ah great, thank you. I kept wanting to say things about “the real world”; apparently I wasn’t completely off base! | |
| Apr 21, 2021 at 20:50 | comment | added | Joel David Hamkins | It can only be independent when it is not true. So there is some nonstandard model of ZFC where $g=1$, but in our universe, $g\neq 1$. | |
| Apr 21, 2021 at 20:48 | comment | added | HJRW | Along the lines of IJL’s answer, I’m confused. Apologies for a naive question! If an explicit g=1 in an explicit group, then that can be proved by writing out a finite string of identities, so wouldn’t ZFC prove that? Then how could it be independent of ZFC? | |
| Apr 21, 2021 at 20:45 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 15 characters in body
|
| Apr 21, 2021 at 20:44 | comment | added | Joel David Hamkins | Yes, this is right. I have now edited. | |
| Apr 21, 2021 at 20:40 | comment | added | Burak | I don't want to sound picky but I feel the need to add in the comments that when Joel says "a theory" it is assumed to be computably enumerable, since, otherwise, the algorithm in the proof would not contradict undecidability of $A$. | |
| Apr 21, 2021 at 20:13 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 115 characters in body
|
| Apr 21, 2021 at 19:42 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 1 character in body
|
| Apr 21, 2021 at 19:36 | history | edited | Joel David Hamkins | CC BY-SA 4.0 |
added 854 characters in body
|
| Apr 21, 2021 at 19:21 | history | answered | Joel David Hamkins | CC BY-SA 4.0 |