Are there any undecidability results that are not known to have a diagonal argument proof?

Question

Is there a problem which is known to be undecidable (in the algorithmic sense), but for which the only known proofs of undecidability do not use some form of the Cantor diagonal argument in any essential way?

I will freely admit that this is a somewhat ill-formed question, for a number of reasons:

1. One could take a proof that does not use diagonalization, and insert a gratuitious invocation of the diagonal argument to avoid a positive answer to this question on a technicality. (Hence the qualifier "essential" in the above question has to do a lot of heavy lifting.)
2. As pointed out by Timothy Chow in this previous MO answer, there is no well-defined notion of what it means to "use diagonalization".
3. Many undecidability results do not mention diagonalization at the top level of their proof, but rely on reductions to other undecidability results, such as the undecidability of the halting problem, which are usually proven by diagonalization.

Nevertheless, I hope the spirit of the question remains clear, despite its ill-posedness.

Two remarks:

1. The undecidability of the halting problem itself certainly has proofs that arguably do not invoke diagonalization (some of them are listed here). But this would not be a positive answer to my question, because the undecidability of the halting problem also has the textbook proof that does use diagonalization.
2. There are certainly undecidability results that are not proven simply by reduction to the halting problem; see the answers to this previous MO question for several examples. It's possible that one of the results mentioned there is already a candidate answer to my question, though I was not able to readily identify such a candidate.

Answer 1

Let me propose a candidate: Kolmogorov complexity is not computable.

That is, there is no computable procedure that, given a finite sequence $s$, produces the size of the smallest program (with respect to some fixed natural notion of size) that can write $s$ as output.

To prove this, we suppose toward contradiction that Kolmogorov complexity were computable. The program doing it would have some size $k$, which we may assume is already rather large. Using this Kolmogorov algorithm as a subroutine, we write down a simple program $p$ that considers the finite binary sequences in turn, until it finds a sequence $s$ having Kolmogorov complexity exceeding $2^{2^k}$. We halt and output the first such $s$ that is found.

Note that $2^{2^k}$ has Kolmogorov complexity much less than $k$, since $k$ can be described explicitly in a program of size about $\log(k)$ by hard-coding the digits, and then we can describe how to compute exponentials. So program $p$ will have size a little more than $k+\log(k)$. Certainly less than $2^{2^k}$.

But if the Kolmogorov computation works correctly, program $p$ outputs a sequence that cannot be produced by such a small program. Contradiction.

Is this proof by diagonalization? Well, at no point did we design a process that diagonalized against all programs, or against all sizes. We didn't do something with every possible index $i$ in order to defeat that particular index as a solution. The program $p$, after all, was designed specifically to defeat only a specific $k$, the size of the program deciding Kolmogorov complexity, which came to us before we designed $p$.

On the other hand... I take a very broad of diagonalization, and on my view almost every nontrivial argument in the subject of logic as a whole, including every undecidability result and every result in computability theory, complexity theory, large cardinal set theory, and so forth, partakes deeply of diagonalization. So what I expect is that for every proposed answer to the question, it will be possible to see a glimpse of diagonalization inside it. It is part of the DNA of the subject.

Answer 2

From a point of view your question relates to an "open conjecture" in computability theory.

I think you are asking if there is a specific problem $P$, which can be shown to be undecidable, but not with a diagonalization argument or with a reduction to the Halting problem which has a diagonalization argument already.

Now let's break this down. A particular decision problem corresponds to a particular Turing degree $T$, and if it's unsolvability can be reduced to the unsolvability of the halting problem, then $T \geq 0'$.

There is an informal conjecture (which I first heard from Steven Simpson, but I don't know who first observed it): The only Turing degrees with nice definitions are $0$ (computable things), $0'$ (things equivalent to the Halting problem), $0''$ (things equivalent to the halting problem relative to the halting problem), and so on. So the only nice non-computable Turing degrees all compute the Halting problem. This includes well known undecidability results like Hilbert's 10th problem, Wang tiling, Kolmogorov complexity, and the like. Solving all of them would solve the Halting problem (which is proved by diagonalization).

Now, we can define other Turing degrees explicitly, like the degree coming from a proof of Friedburg-Munich theorem that there is a degree between $0$ and $0'$, but the definitions are incredibly connected to the exact definitions we give of things like Turing machine. Even a slightly different (but equivalent) definition of Turing machine would lead to a different enumeration of all programs, which would lead to a very different intermediate degree.

The conjecture is basically that there are no real (mathematical) world problems which are aren't in $0$, $0'$, $0''$, or higher. Of course, like your question, this conjecture isn't well-posed. (But I have heard people suggest that the solution to Hilbert's 10th problem for rationals is an intermediate degree between $0$ and $0'$ which seems ludicrous to me, as it would clearly violate this conjecture.)

So I think no, there are no (natural) undecidability problems which can't be solved by diagonalization, even if it is just reducing it to the Halting problem.

Answer 3

Too long to be a comment: Joel's Kolmogorov complexity argument contains what I would consider to be a diagonalization. Here is an essentially equivalent argument which makes the diagonalization more obvious, by removing the use of contradiction and just arguing directly:

Theorem: No program computes Kolmogorov complexity.

Sketch. Let $P$ be a program which takes binary strings as input and outputs numbers; we will construct a binary string $s$ whose Kolmogorov complexity satisfies $K(s) \neq P(s)$. We will do this by constructing a second program $Q$ as in Joel's argument, which uses $P$ as a subroutine to output the lexicographically first string that satisfies $P(s) \ge 2^{2^k}$ where $k$ is the size of $P$, if there is one.

If there is, then as Joel argues, $Q$ cannot be much larger than $P$, which gives us a bound along the lines of $K(s) \le k + \log k + C$ or something like that. And, up to cleaning up the details of the various bounds (we could replace $2^{2^k}$ by a different function if necessary), this gives $K(s) < P(s)$ as desired.

Otherwise, $P$ is bounded by $2^{2^k}$, but $K$ is not, so we can find a string $s$ such that $K(s) \ge 2^{2^k} > P(s)$. $\Box$

To my mind this is a diagonalization over all programs, and I think writing out the argument in more detail it would look even more like a diagonalization. After all, at some point in the search over binary strings, in order for this argument to work, $Q$ necessarily comes across $P$'s source code in binary, and applies $P$ to it!

Answer 4

I think that the Burali-Forti-like proof of the incomputability of (a minor variation of) Kleene's $\mathcal{O}$ may fit the bill.

Let $\mathcal{W}$ be the set of indices for computable well-orderings; basically, $e\in\mathcal{W}$ iff the $e$th Turing machine computes a binary relation $R$ on the naturals such that $(\mathbb{N};R)$ is a well-ordering (which I'll conflate with $R$ itself). Consider - before setting up any counterfactual hypotheses - the well-ordering $$\lambda:=\left(\sum_{e\in\mathcal{W}}R_e\right)+1.$$ By definition, every computable ordinal embeds as a proper initial segment of $\lambda$, so $\lambda$ is not isomorphic to any computable ordinal. But we can clearly compute a copy of $\lambda$ from $\mathcal{W}$. Note that at no point do we have to look at the putative index for a computation of $\mathcal{W}$ or $\lambda$, so I don't see anything like diagonalization here.

---

There are two sticking points here:

• Does the above genuinely avoid diagonalization? I would argue that it does, and in particular that the definition and analysis of $\lambda$ doesn't involve any self-reference since a putative index for $\mathcal{W}$ hasn't even been introduced yet, but see the comments below.

• Even if the argument above is diagonalization-free, we still have the question of whether some proof of the incomputability of $\mathcal{W}$ uses diagonalization. For instance, it's certainly possible to prove the uncomputability of $\mathcal{W}$ by first reducing ${\bf 0'}$ to $\mathcal{W}$ and then applying a diagonal argument to analyze ${\bf 0'}$. However, I think this is so much more involved than the above purely structural argument that this could be said to not benefit from diagonalization.

Ultimately I think this holds up to both points, but one's mileage may vary.

Answer 5

[Edited slightly for (hopefully!) greater clarity.]

This is more of a comment than an answer, but I think it is relevant. In the context of computational complexity theory (rather than computability theory), one might hope that it would be easier to give examples of theorems whose proofs not only don't use diagonalization, but can't use diagonalization. The reason is that the conventional wisdom is that "diagonal arguments relativize," and hence a diagonal argument cannot prove something like $\mathsf{P} \ne \mathsf{NP}$, which has contradictory relativizations.

Unfortunately, even the case of $\mathsf{P} \ne \mathsf{NP}$ is not clearcut, because it's not entirely clear exactly what a "diagonal argument" is. In a very interesting paper, Indexing of subrecursive classes, Dexter Kozen argued that if $\mathsf{P} \ne \mathsf{NP}$ is provable at all, then it is provable by diagonalization. Of course, you could object that Kozen's definition of a "diagonal argument" is artificial, and that there should still be some sense in which the conventional wisdom is correct. But pinning down that sense is surprisingly subtle, especially if a diagonalization argument is combined with other arguments. In Scott Aaronson's chapter of the book, Open Problems in Mathematics, he sketches the proof of a famous lower bound due to Ryan Williams, and concludes:

Williams’s result makes it possible to imagine that, in the far future, $\mathsf{P} \ne \mathsf{NP}$ might be proved by assuming the opposite, then deriving stranger and stranger consequences using thousands of pages of mathematics barely comprehensible to anyone alive today—and yet still, the coup de grâce will be a diagonalization argument, barely different from what Turing did in 1936.

Anyway, even if we set aside the reverse-mathematical issues that I mentioned in that other MO answer, the bottom line is that it may be very difficult to convincingly argue that a particular uncomputability proof "does not use the diagonal argument in any essential way."

Answer 6

This is not really an answer but a possible way to formalize your question. In my mind the “essence” of a diagonal-style proof of undecidability is that it explicitly points out the input on which every potential machine fails to solve the given problem: if $\mathcal{L}$ is our hard language/function, the proof of undecidability gives a constructive procedure that takes the code for any purported machine $M$ solving $\mathcal{L}$, and exhibits a (list of) input(s) where a mistake must occur. The following is a straightforward way to formalize this, and I think it captures a rather broad notion of “diagonalization-style” undecidability proofs:

Definition. Let $\mathcal{L} \subseteq \{0,1\}^*$ be a language. A "certifier" for the undecidability of $\mathcal{L}$ is a total computable function $\mathcal{C}$ which has the following behavior. On input a machine description $M$, $\mathcal{C}(M)$ prints out a list of inputs $x_1,\ldots,x_k \in \{0,1\}^*$ such that for some $i \leq k$, $M(x_i) \neq \mathcal{L}(x_i)$ (i.e. either $M$ loops forever on $x_i$ or else $M$ halts with the wrong value on $x_i$). We say $\mathcal{L}$ is "certifiably undecidable" if it has a certifier.

Basically the same concept has been studied in complexity theory under the name "refuter," e.g. here.

It is easy to see that the halting problem is certifiably undecidable using the classical argument; from the description of purported halting-problem solver $M$ we can construct the dialgonal machine $D_M$ using $M$ as its halting test; then $\mathcal{C}(M)$ can output $\langle D_M,D_M\rangle$. In the case of Kolmogorov complexity, given $M$ we can choose $n$ sufficiently larger then the description length of $M$ and output all strings of length $n$; a basically identical argument works for Busy Beaver.

It is also straightforward to see that the certifiably undecidable languages are upward-closed under computable truth table reductions; if $\mathcal{L} \leq_{tt} \mathcal{L}'$ we can transform the certifier for $\mathcal{L}$ into one for $\mathcal{L}'$ by enumerating queries made when we compose the certifier with the reduction. This holds also for a stronger notion of reduction where oracle queries can be made in sequence, but the total number of oracle queries is bounded above in the input length by a total computable function; I am not sure about a general Turing reduction.

In this framing your question can be formalized as: is every undecidable language certifiably undecidable? If there is a counter example then it must be intermediate between $0$ and $0'$, at least with respect to the restricted notions of reducibility mentioned above. I have no idea whether any of the known intermediate languages are a good candidate for this.

Answer 7

EDIT: On reflection, this answer is pretty incorrect. There is a point here, but it's formulated badly enough that I think this should be ignored. I wasn't sure what best practice is for a wrong answer, so I'm going to leave a comment with corrections.

Forgive both the late reply and potentially sophomoric comment, but maybe it would help to break down the Lawvere theorem and ask whether a non-diagonal undecidability proof is constructible.

An undecidability proof has the rough anatomy that we want to find some epimorphism $g: A \to Y^S = g: A \to S \to Y$ such that the image of $g$ is monomorphic. In the usual case that $A = S$ is a set and $Y$ is a finite set, $g$ picks out some $h: A \to Y$ that assigns some $y \in Y$ to each $a \in A$, or in other words, $g$ finds, for each $A$, some $h$ that decides $a$s. We then find that assuming such an epimorphism exists, we obtain a contradiction, thus $A$ is not in general decidable.

Undecidability proofs are, I think anyway, quintessentially nonconstructive, so we have to assume decidability (i.e., there exists a $g$) and show it leads to contradiction (whether explicitly or not) in order to get an undecidability proof. Assuming there exists an epimorphism $g$ is a strictly necessary element.

Then, just by uncurrying, we can show that $g$ is isomorphic to $f: A \times S \to Y$. Then, the diagonal morphism $\Delta: A \to A \times S$, which forms an identity pairing $\Delta(a) = (a, a)$ in the usual case, does not add much, as $f \circ \Delta$ is isomorphic to $g \circ id_A = g$ (more generally, $f \circ \Delta$ is isomorphic to some $g \circ i$ where $i: A \to A$ is an isomorphism). Joel's reply above suggested that the application of the diagonal morphism could be thought of as a pivotal step in singling out a diagonalization, but it seems to me to be really trivial. At best, non-diagonal proofs seen this way apply an isomorphism $A \to A$ before doing their work.

At this stage, I think most of a diagonalization proof is necessary, including, in effect, the diagonal part, in order to show undecidability. At least, if we find a proof that doesn't seem to involve diagonalization, we can be pretty well assured that it should not be too hard to transform it into an argument that uses a $\Delta$.

The final step in the diagonalization is to choose $\alpha: Y \to Y$ without any fixed points. Since we can choose such an $\alpha$, by applying $\alpha \circ f \circ \Delta: A \to Y$, we show that $f \circ \Delta$ is not unique up to isomorphism $A \to A$, and so $g$ cannot be an epimorphism. If we're looking for alternatives to diagonalization, the place might be here. There might be a nontrivially different approach to showing that $g$ cannot be an epimorphism. Though, for undecidability results, I have a hard time imagining how one proves that one cannot find an $h$ that decides arbitrary $a$ other than choosing $\alpha \circ h$ that makes some sort of inverse decision assignment.

To make a long answer short, if I haven't made some basic error, I think the answer to the question may be "no, and furthermore, there can't be".

Corrections:

1. An instance of an undecidability proof assumes the existence of a unique morphism $g: A \to Y$. Assuming $g: A \to S \to Y$ is already almost all of the heavy lifting in a diagonalization/Lawvere proof, and isn't strictly necessary to prove undecidability.
2. To get from undecidability to Lawvere, we let $g = h \circ k \circ id_A: A \to A \to S \to Y \sim A \to A \times S \to Y$, where $k$ is an isomorphism. For instances where $S = A$, $k$ is trivial as the above suggests (and could just as well be the identity), but that might not always be so.
3. For $g$ to be unique, $g \equiv \alpha \circ h \circ k \circ id_A \sim \alpha \circ f \circ \Delta$ for any choice of $\alpha$, but, since we may always choose $\alpha: Y \to Y$ with no fixed points (as $Y$ is nondegenerate), this cannot be.

So here is the rub. $k$ might not always be trivial (though these are cases where we want to move to $S$ because it's easier to make claims about $S \to Y$ than $A \to Y$), but if we have a proof that there does not exist a unique morphism $g$, then we can always transform this into a proof about $g \circ id_A \circ id_A \sim f \circ \Delta$. However, I can imagine cases where doing so is unnecessary and this move seems superfluous. Though it doesn't seem to me to be whenever $g = h$ (e.g. the halting problem), so maybe that's just a trick of the light.

I'm still not sure that I've got this right, but I think it's at least worthwhile to admit the mistake.