What do you do if you believe a problem is undecidable? While the title of this question is subjective, I hope to make what I'm looking for quite concrete.  The first, and main question is this: If you believe that a problem you are working on is formally undecidable, but you are not a logician, what are some ways to begin learning the tools necessary for you to try to prove undecidability?  Where should one begin?
Now, for an explicit example.  In ring theory one of the big open problems is called Koethe's conjecture.  There are many equivalent ways to state the conjecture such as "The sum of two nil left ideals is still nil."  Let me give another equivalent description.
Let $R=\mathbb{Z}\langle a,b\rangle$ be the free ring on two non-commuting generators.  Suppose that $I$ is a left ideal of $R$, containing some power of $b$, and containing some power of every element of $Ra$.  Then the conjecture asserts $I$ contains some power of $a+b$.  Note that $R$ is countable, and in fact we can easily enumerate the elements of $Ra$ as $f_1,f_2,\ldots$.
Thus, given any sequence of positive integers $\vec{n}=\{n_0,n_1,n_2,\ldots\}$, the conjecture asserts that the left ideal containing $b^{n_0},f_1^{n_1},f_2^{n_2},\ldots$ also contains a power of $a+b$.
For some sequences $\vec{n}$ (such as eventually constant sequences), it is not difficult to compute that the conjecture is true.  But in general the computations get extremely difficult.  Lam says in his "First Course in Noncommutative Rings" p. 171, that there has been a 

(long-held) suspicion that the Conjecture is false.

If so, then it is false for a sufficiently fast growing sequence $\vec{n}$.
However, one of the troubles here is that nobody knows how to control the behavior of $I$ for fast growing sequences $\vec{n}$, and there are also ways to modify $I$ only slightly and provably not produce a counter-example.
My current hunch is that the conjecture is false, but to see this we need tools to assert that (for fast growing vectors $\vec{n}$) the ideal $I$ stays complicated.  I'm not confident that the regular tools from ZFC are sufficient to the task; but have no idea where to go from here.
One last comment: There is always the danger of fearing that a problem one is working on is formally undecidable, just because you can't immediately solve it.  Because of this I haven't given up hope that there is such a solution.  However, there is also the chance that some stronger set theory may provide tools to look at the problem differently, and really that's what I'm after.
 A: Joel David Hamkins has given a good answer in the case of (2), where a certain notion when expressed formally in the language of a theory $T$ (and also the negation of this notion) may not be provable from $T$ using the appropriate proof system.  I would like to touch on the other case (1), where it may be possible to show not only that the conjecture is false, but that it can be false in a noncomputable way.  This would be a good resolution from the standpoint of the original poster, because it would shed light on the nature of algorithmic questions in general algebra.
(Disclaimer: In spite of my proximity to the subject, I am no expert on decidability.  I recommend Algorithmic Problems in Varieties by Sapir and Kharlampovich, and also section 6 and earlier of Ross Willard's "An Overview of Modern Universal Algebra", both available on the Web.  I had the privilege of being one of the first to see McKenzie present his work on Tarski's Finite Basis Problem: that work influences this post.)
Consider the possibility that Koethe's conjecture is false.  As Pace Nielsen points out in his question, one way that it could be false is that there exists a fast growing sequence $n_i$ and a (hopefully recursive) enumeration $f_1,f_2, \ldots$ of $Ra$ such that $a+b$ and all of its powers  avoids all the left-ideals generated by a finite subsequence of $b^{n_0}, {f_1}^{n_1}, {f_2}^{n_2}, \ldots$ .  (Unless I missed something, this should be equivalent to his formulation.)  It would be nice to be able to characterize those ideals which fail the conjecture, or given a particular ring, to characterize those sequences and enumerations which lead to failure.
As mentioned in the comments, to show that no recursive characterization is possible, one method would be to reduce an undecidable problem to this question.  In other words, construct a recursive map $\phi$ so that for every instance $I$ of a problem known to be undecidable, $\phi(I)$ is a sequence (say) of exponents $n_j$ such that a certain enumeration of $Ra$ raised to exponents $n_j$ produces an ideal which contains a power of $a+b$ iff $I$ satisfies the property in the problem known to be undecidable.  The Boone-Novikov result is well known (a finitely presented group with undecidable word problem), and the article of Sapir and Kharlampovich contains many more examples, and if the Koethe problem "looks" enough like one of the undecidable problems, one might then construct a recursive $\phi$ as suggested above.
Alternatively, one could have a mastery of the situation that one could try to build a sequence of ideals with such a property that "encoded" Turing machine computations.  In the case of Tarski's Finite Basis problem (is there a computer program that can take as input the function tables of a finite algebra A of finite type, and output "yes" if the equational theory of V(A) is finitely-based, and "no" otherwise), there was a series of related problems that McKenzie was working on that allowed him to express a Turing program as an algebra with certain operations corresponding to the state transition table of the program, such that if the halting state were reached, that would correspond to a certain algebraic property in an infinite power of the base algebra, and not correspond otherwise.  The properties involved had to do with residual smallness, and McKenzie told me that part of his thought process was to arrange all of the properties he needed in small groups, and make small changes in the algebraic construction to get the group of properties he needed (my wording based on a poor remembering of an event over twenty years in the past).
This is an attempt then to answer the question in a different way: if you suspect the answer is not just no, but no in a non-recursive way, try two approaches: reduction from something in Kharlampovich-Sapir (or other sources), or understand the properties of the ideals that satisfy Koethe's conjecture as well as those that don't, and see if those properties are recursively inseparable (can be related somehow to computations halting or not).
Gerhard "That's How I Would Start" Paseman, 2015.03.24
A: The first thing to say is that for a statement to be independent
of some axioms means really two things, namely, that it is
consistent with those axioms, and also that the negation of the
statement is consistent with those axioms. And typically, the
proofs of these two things are essentially unrelated. So in your
case, where the question appears to be open, I would say that it
is somewhat premature to speculate about full independence, when
instead you should speculate about the consistency of the
statement, or the consistency of the negation of the statement.
Independence occurs only when both of these situations are the
case.
The second thing to say is that of course almost every nontrivial
statement is independent of some very weak set of axioms; you
didn't specify which axiomatic system you were considering for
independence, but the nature of the independence proofs varies
quite a lot depending on the system that one is considering.
Often, statements that are proved independent of PA or some other
weak system are provable in ZFC, and similarly a statement that is
independent of ZFC might be provable from ZFC plus large cardinals
or some other strong system. No statement is independent in any
absolute sense, since in the theory taking a position on that
statement, it becomes settled. So the property of a statement
being independent is only sensible relative to a particular
axiomatic system.
Furthermore, I would say that the philosophical significance of an
independence result can vary quite a bit depending on the
background system for which it is established. To my way of
thinking, the fact that PA does not prove, say, that $\epsilon_0$ is
well-founded is less troubling philosophically than the fact that
CH and many other statements appears to be unsettled by ZFC plus
any of the known large cardinal axioms, which are consistency-wise
the strongest theories we know about, since in the first case we
might look upon it simply as a weakness of PA, but in the latter
case we appear to be left with some angst about what is the real
truth of the matter of CH.
So let me discuss the way a set theorist approaches the
possibility of independence. These are some of the questions that
come to mind when considering the possibility of independence.
Is the statement something that could be changed by forcing?
The overwhelming majority of known independence results in
mathematics are ZFC independence results established by the method
of forcing. Almost every natural nontrivial statement of infinite
combinatorics has been proved to be independent of ZFC by forcing,
and we have an enormous number of naturally occuring statements in
mathematics that are known to be independent of ZFC.
Nevertheless, in some cases, we can tell that a statement can
definitely not be shown independent by means of forcing,
simply because of its logical complexity. Specifically,
the Shoenfield absoluteness theorem shows that
any $\Sigma^1_2$ statement is invariant by forcing.
For example, in the case of your example, it appears to have
complexity $\Pi^1_1$, and this means that your statement is
invariant by forcing. Thus, it will not be possible to prove your
statement independent of ZFC by means of forcing. This doesn't
mean it isn't independent of ZFC, but it will not be proved
independent of ZFC in the way that most statements known to be
independent of ZFC have been proved to be independent of ZFC.
Is the statement something that become settled if a certain set
were to become countable? Any given set can become countable in
a forcing extension, and this situation often settles many
specific statements.
Is the statement settled by the continuum hypothesis, or by
Martin's Axiom? Many statements can be proved consistent by
being a consequence either of the continuum hypothesis or the
generalized continuum hypothesis or by Martin's axiom or other
axioms that are known to be relatively consistent with ZFC. This
is a very common way for non-set-theorists to establish
consistency results, by proving that the statement they are
considering are simply a consequence of statements about which
consistency results are already known.
Is the statement a consequence of the existence of large
cardinals? Does it imply the existence or consistency of large
cardinals? Sometimes it happens that the existence of large
cardinals can imply the truth or consistency of a given statement,
or a given statement implies the truth or consistency of lesser
large cardinals, and in this way the consistency of the statement
fits into the large cardinal hierarchy. This has consequences for
independence. For example, if every set of reals is Lebesgue
measurable, then $\omega_1$ is inaccessible to reals, and so the
consistency of that situation with ZF implies the consistency of
an inaccessible cardinal with ZFC. It follows that we cannot prove
even in Con(ZFC) itself (if this is consistent) that ZF does not
prove the existence of a Lebesgue non-measurable set. There are
many similar situations, where a given statement $\varphi$ might
imply the existence of an inner model with a given large cardinal,
and so it follows that the consistency of the statement cannot be
proved without assuming at least the consistency of that large
cardinal hypothesis.
For independence over weaker systems, such as the usual systems of
second-order number theory, there are another whole list of
questions that one would ask, and I would expect that some other
MO users might elaborate on this. For example, Is the statement
something that would be settled in the world in which everything
is computable? If not, the statement has a hope to be
independent of $\text{RCA}_0$, which is the universe of
second-order number theory consisting essentially of computable
sets only.
Ultimately, to prove that statement $\varphi$ is independent of
theory $T$ means to prove both that $T+\varphi$ is consistent and
also $T+\neg\varphi$, and so one needs to appreciate the depth and
subtlety of consistency proofs for the various theories $T$ that
might be under consideration.
