6
$\begingroup$

Edited (this question contains two versions of a similar question)

Is there some finitely presented group $G$ generated by $g_1,...,g_n$ such that there is an element $g\in G$ expressed as a finite word in $g_i$'s so that it is impossible to prove neither $g=1$ nor $g\ne 1$?

Is such a group $G$ exists, what would be a relatively simple example?

Adjusted question. Is there $G,g$ so that $g\ne 1$ in $G$ but is it impossible to prove this in finite time?

Improve this question
$\endgroup$
11
  • $\begingroup$ Two words $u,v$ in the generators represents the same element of $G$ iff $uv^{-1}$ represent 1. Hence it seems to me your question reduces to the existence of finitely presented group whose word problem is unsolvable, of which there are many known examples. $\endgroup$
    – Adrien
    Commented Feb 17, 2013 at 15:12
  • 1
    $\begingroup$ I am not sure I understand correctly what you want for question 2. Can you not take a Turing machine M for which it is undecidable if M halts on input its Gödel number <M> and then encode this into a finitely presented group for which there is a single input for which there is no finite time proof whether it is not 1? $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 16:29
  • 1
    $\begingroup$ About adjusted question: if $g=1$ in $G$, then it is impossible to prove that $g\ne 1$. You probably want $g\ne 1$ but such that there is no proof of that fact. $\endgroup$
    – user6976
    Commented Feb 17, 2013 at 16:30
  • 2
    $\begingroup$ In other words the usual proof of Godel's incompleteness gives a fixed statement for which there is no finite proof. Encode this into a finitely presented group in the usual way. $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 16:38
  • 2
    $\begingroup$ I don't agree that Mark's answer answers the original question. Usually when one speaks of "proof", one is speaking of a finite combinatorial object, so I don't really understand how the adjusted question differs from the original question. To be sure, there are various infinitary proof systems, but one shouldn't really be vague about ones' infinitary logic, if that was the intended context. (Lastly, I read "neither/nor" in the question as "either/or", with the meaning that it is impossible to prove $g=1$ and also impossible to prove $g\neq 1$, which seems to be what is intended.) $\endgroup$
    – Joel David Hamkins
    Commented Feb 17, 2013 at 17:06

3 Answers 3

Reset to default
15
$\begingroup$

Let me offer another way to explain a similar idea as in Benjamin's answer.

The answer to the original question, as well as the updated question, is Yes, there is such a finite group presentation.

Since you are asking whether or not a given assertion is "provable", you should be explicit about the theory in which you are making such proofs. Let's suppose that you intend us to use one of the standard default background theories, such as ZFC or ZFC + large cardinals or whatever. Such theories have a computably presentable list of axioms.

Now, consider the standard proof that the word problem is not decidable. The way this is proved, one fixes any Turing machine $M$, and writes down a finitely presentation of a group $G_M$, whose words in effect simultate the comptuation of $M$. The result is that there is a generator $g$ of the presentation such that $g=1$ in the group if and only if $M$ halts (on empty input). Thus, we reduce the halting problem, which is undecidable, to the word problem, and so the word problem is undecidable.

But now for the given background theory $T$, there will be an explicit Turing machine $M$, such that the question of whether $M$ halts is not provable in $T$ (for example, imagine the Turing machine that searches for a proof of a contradiction in $T$). Since $T$ does not prove whether $M$ halts or not, it follows that $T$ will neither prove nor refute the corresponding assertion about whether $g=1$ or not in the group presentation $G_M$.

In this example, there will be no proof that $g=1$ and no proof that $g\neq 1$.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Joel, thank you for this detailed answer! (I will need some time to understand it) $\endgroup$
    – aglearner
    Commented Feb 17, 2013 at 18:43
  • 1
    $\begingroup$ @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. $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 20:02
  • 1
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Feb 17, 2013 at 20:18
  • 1
    $\begingroup$ 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$. $\endgroup$
    – Joel David Hamkins
    Commented Feb 17, 2013 at 20:24
  • 1
    $\begingroup$ Basically a yes to the original question automatically builds a yes to the second because the unprovable thing must be in the no part. $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 20:42
10
$\begingroup$

The following is an abridged translation of a philosophical digression from my lectures on Group Theory (in Russian).

Metatheorem 3.5.1. For any finite (group) presentation $G$ with non-solvable word problem, there exists a word $w$ (called bad) such that it is possible to prove neither that $w=1$ in $G$ nor that $w\ne 1$ in $G$.

Proof. Note that any reasonable definition of the notion of proof has the following property:

Any proof can be written in some fixed formal language; and there exists an algorithm VERIFICATION, which takes as input any text in this language and any assertion (also written in this language) and says whether or not the given text is a proof of the given assertion.

Suppose now that there are no bad words for a given presentation. Then it is easy to construct an algorithm solving the word problem: for any input word $v$, we simply search all texts and feed them to the algorithm VERIFICATION until we find a text which is either a proof that $v=1$ in $G$ or a proof that $v\ne1$ in $G$.

Remark. Any word equal to a bad word in the group $G$ is bad itself (because for any two words equal in $G$, their equality can always be proven).

So, we can speak about bad elements of a group (not only bad words). Moreover, it is easy to show that the badness of an element $g\in G$ does not depend on the choice of finite presentation of $G$.

As a corollary, we obtain the following strange-looking fact.

Metatheorem 3.5.2. Any bad word is, actually, not equal to 1.

(Because 1 is not a bad element, obviously.)

Although bad words exist, no particular example can be constructed.

Metatheorem 3.5.3. For any bad element, it is impossible to prove that this element is bad.

Proof. Indeed, a proof of the badness of an element $g$ would prove, in particular, that $g\ne1$ (by Metatheorem 3.5.2) that contradicts the definition of a bad element.

A similar argument and the Adyan$-$Rabin theorem show that:

  • There exists a bad group, i.e. a finitely presented group such that it is possible to prove neither that this group is trivial nor that this group is non-trivial.

  • Each bad group is non-trivial.

  • For any bad group, it is impossible to prove that this group is bad.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Your theorem order looks strange to me (and OP question too). If $g=1$, clearly, there is a proof of this fact (in every strong enough theory). So, the correct question whether there exists a proof of $g \neq 1$ if $g$ is actually not 1. The answer is - for every particular theory unprovable $g\neq 1$ exists (otherwise we could solve wp). That's all. $\endgroup$
    – Dan
    Commented Apr 23, 2014 at 21:08
  • 1
    $\begingroup$ @Dan, surely. What you said is basically Metatheorem 3.5.2 from my answer. $\endgroup$
    – Anton Klyachko
    Commented Apr 24, 2014 at 22:04
5
$\begingroup$

For the adjusted question, take a group G with generators $x_n$ and relations $x_n=1$ if the statement with Gödel number n is provable. (This is recursively presented because you can enumerate all proofs.) Higman embed G into an fp group H. Take a Gödel number m of a statement which is true but not provable (exists by incompleteness). We cannot give a finite proof that $x_m\neq 1$ in H.

edit Following Joel's kind suggestion I should use Rosser sentences instead of Gödel sentences to be independent of the background meta theory.

Improve this answer
$\endgroup$
6
  • $\begingroup$ I'm assuming finite proof is defined and a finite proof of the group theory fact can be then unwound to the arithmetic one. $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 16:53
  • $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Feb 17, 2013 at 16:56
  • $\begingroup$ 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$. $\endgroup$
    – aglearner
    Commented Feb 17, 2013 at 16:57
  • $\begingroup$ 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$. $\endgroup$
    – Joel David Hamkins
    Commented Feb 17, 2013 at 17:13
  • $\begingroup$ 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 $\endgroup$
    – Benjamin Steinberg
    Commented Feb 17, 2013 at 17:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .