An element $g$ in a group such that neither $g=1$ nor $g\ne 1$ can be proved. 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? 
 A: 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.
A: 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.
A: 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$. 
