What do you do if you believe a problem is undecidable?

Question

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.

Answer 1

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.

Answer 2

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