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.