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.
  • 3
    $\begingroup$ I would argue that the 1-genericity argument for the undecidability of the halting problem is just laundering some underlying diagonalization. Why isn't a 1-generic computable? Because it generically diagonalizes against all computable reals. $\endgroup$ Sep 6 at 17:32
  • 9
    $\begingroup$ Not an answer, but it may be worth recalling that it is consistent with intuitionistic ZF (or similar constructive frameworks) that all functions $\mathbb{N}\to\mathbb{N}$ are computable: while this doesn't say we need a diagonal argument to construct a noncomputable $\mathbb{N}\to\mathbb{N}$, at least we'll need to use excluded middle (e.g., in the form “every given Turing machine (+input) either halts or does not halt”). $\endgroup$
    – Gro-Tsen
    Sep 6 at 21:09
  • 3
    $\begingroup$ @TerryTao To my way of thinking, the essence of diagonalization is that one seeks to construct an object meeting a certain number of requirements, which can be enumerated in some sense, and one can undertake a construction of the object in the same length as that enumeration, fulfilling the $\alpha$th requirement at stage $\alpha$ of the construction. $\endgroup$ Sep 7 at 0:10
  • 13
    $\begingroup$ We can represent problems as real numbers. There are only countably many diagonal arguments (since arguments must be finite length), and thus we can pick an uncomputable real number such that it's nth digit is different than the nth digit of the nth uncomputable real number with a diagonal argument. ... Oh wait. $\endgroup$
    – PyRulez
    Sep 7 at 16:04
  • 2
    $\begingroup$ @ZuhairAl-Johar Hence the qualifier "some form of". $\endgroup$
    – Terry Tao
    Sep 9 at 1:44

7 Answers 7


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 less than $k$ or about $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.

  • 12
    $\begingroup$ Nice example. I guess I can accept this type of argument (and similar "Berry's paradox" type arguments) as not strictly being a diagonal argument, though it certainly has a similar "self-defeating object" flavor to it, and I can't see a natural way to replace it with a more obviously diagonalization style argument. $\endgroup$
    – Terry Tao
    Sep 6 at 18:39
  • 2
    $\begingroup$ I also take an extremely broad view of diagonalization, but I'm actually struggling to come up with examples in model theory of arguments that I would consider to really be descended from diagonalization. (Of course there are a few people both inside and outside of model theory who don't really consider it 'logic' at this point, but that's a separate issue.) $\endgroup$ Sep 6 at 19:04
  • 11
    $\begingroup$ But we can also show that Kolmogorov complexity solves the halting problem, and the halting problem isn’t computable, so Kolmogorov complexity isn’t computable. So transitivity it has a proof (not the standard one) by diagonalization. $\endgroup$
    – Jason Rute
    Sep 6 at 19:28
  • 8
    $\begingroup$ @JasonRute I'm looking up the proofs of the reduction of the halting problem to the Kolmogorov complexity problem and they seem to rely on the Berry type argument that Joel provided in order to justify the reduction. If so, then I would say that this is a "gratuitious" way to shoehorn in a diagonalization. Do you know of a proof of reduction that doesn't contain something resembling Joel's argument? $\endgroup$
    – Terry Tao
    Sep 7 at 1:22
  • 3
    $\begingroup$ I have provisionally accepted this answer as the leading candidate currently proposed for an undecidability result whose known proofs, while certainly containing diagonalization-like themes, do not seem to contain diagonalization (as narrowly interpreted) as an essential component. But I admit that this is a somewhat subjective call, and am open to being persuaded to other points of view. $\endgroup$
    – Terry Tao
    Sep 8 at 21:53

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.

  • 1
    $\begingroup$ Martin's conjecture. ams.org/journals/notices/201908/rnoti-p1209.pdf $\endgroup$ Sep 6 at 20:28
  • 1
    $\begingroup$ @JoelDavidHamkins Is Martin’s conjecture a formalization of this? In particular, does Martin’s conjecture imply that Hilbert’s 10th problem for rationals can’t be an intermediate degree? $\endgroup$
    – Jason Rute
    Sep 6 at 21:02
  • $\begingroup$ I don't know about that specific consequence, but Martin's conjecture is about the naturality of the jump sequence 0, 0', 0'', in the Turing degrees. In some recent work, I have called for a set theoretic analogue in the hierarchy of consistency strength. $\endgroup$ Sep 6 at 22:28
  • 5
    $\begingroup$ I was going to disagree with this intuition but after more thought I agree. I think there is very little reason to believe that every natural computational problem intermediate between $0$ and $0'$ is provably equivalent to either $0$ or $0'$. But for, say, the rational Diophantine equations problem to be inequivalent to $0$, there would have to exist rational Diophantine equations which have solutions but whose solutions grow faster than any computable functions. It seems unlikely for these to exist if a computer cannot be somehow embedded into a rational Diophantine equation. $\endgroup$
    – Will Sawin
    Sep 6 at 23:58
  • 2
    $\begingroup$ Counterspeculation: maybe natural problems having a degree intermediate between $\mathbf{0}$ and $\mathbf{0'}$ abound (and I don't think it's far-fetched that H10P over the rationals is such), but we don't see them because we utterly lack the means to prove that such an intermediate-degree problem is undecidable, since the only technique we have is basically to reduce to the halting problem (in much the same way that we lack the means to prove that an $\mathbf{NP}$ problem isn't in $\mathbf{P}$); so we just see them as “unknown if decidable” problems. $\endgroup$
    – Gro-Tsen
    Sep 8 at 18:22

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!

  • 4
    $\begingroup$ Nice! Interesting how the operation of removing the use of proof by contradiction, which is basically a triviality in (classical) logic, can dramatically change one's perception of whether an argument is a "diagonal argument". Perhaps one moral to draw from this is that the notion of "using diagonalization" is not really preserved by classical logical equivalence. [And now I recall that I had posted on this topic 13 years ago: terrytao.wordpress.com/2010/10/18/… ] $\endgroup$
    – Terry Tao
    Sep 7 at 3:01
  • 1
    $\begingroup$ Though I don't actually see the "self-referential" aspect of your argument. Do you actually use at any point the fact that space of binary strings $s$ that you chose as the input domain is also the space that encodes programs and is used to define Kolmogorov complexity? $\endgroup$
    – Terry Tao
    Sep 7 at 3:20
  • 4
    $\begingroup$ .. hmm, actually I'm not convinced after all that this is a true diagonalization argument. The program $Q = Q_P$ constructed here only requires knowledge of the program $P$; it is not designed to somehow evade a large class of programs at once, and the fact that the inputs here are the same object type (binary strings) used to encode programs seems to be a red herring. $\endgroup$
    – Terry Tao
    Sep 7 at 3:40
  • 2
    $\begingroup$ You can argue that diagonalization is gratuitous here because we do not need to construct the entire table; we assume for contradiction that there exists a row that computes $f^*$, then show that it does not. (Cantor in some sense requires constructing the entire table before proving the row-wise contradiction.) But then I think we have to admit that diagonalization is gratuitous in the case of the Halting proof as well... $\endgroup$
    – usul
    Sep 9 at 13:49
  • 2
    $\begingroup$ The sentence "for all computable $P$, there exists $s_P$ such that $P(s_P) \neq \mathrm{Halt}(s_P)$" is necessarily part of any proof of the uncomputability of $\mathrm{Halt}$, because this is just a tautological reformulation of what uncomputability means. This isn't the part which is the diagonal argument. The part that is is the quining statement: "Given a computable $H(P,s)$, there exists $K$ such that $K$ halts iff $H(P,P)$ is false". $\endgroup$
    – Terry Tao
    Sep 11 at 15:08

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.

  • 1
    $\begingroup$ I would say this is a typical diagonal argument :D $\endgroup$ Sep 6 at 17:34
  • 4
    $\begingroup$ It feels like if we unpack the fact that "any computable ordinal embeds as a proper initial segment of $\lambda$" you do look at the putative index for $\lambda$! $\endgroup$
    – cody
    Sep 6 at 17:43
  • 1
    $\begingroup$ @cody No, you don't: that fact is proved (and $\lambda$ itself is defined) outside the proof-by-contradiction structure. It's simply a true statement about $\lambda$. I've rephrased things to make this clearer. $\endgroup$ Sep 6 at 17:44
  • 2
    $\begingroup$ @მამუკაჯიბლაძე True, but that has nothing to do with diagonalization. $\lambda$ is a perfectly-well-defined classically-existing object; it, and its basic properties, take place outside any counterfactual assumptions being made. $\endgroup$ Sep 6 at 17:46
  • 1
    $\begingroup$ I really think OP must tell us more. For me, $\lambda$ works by exhausting all possible indices, which for me smells like diagonalization, but I probably cannot say anything more sensible about it. $\endgroup$ Sep 6 at 17:56

[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."


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.


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".


  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.

  • 2
    $\begingroup$ I'm not sure I understand your claim that undecidability proofs are "quintessentially nonconstructive." Do you just mean that they involve proof of negation? $\endgroup$ Sep 11 at 14:58
  • 1
    $\begingroup$ @TimothyChow I think that would be accurate, thank you. I was referring to the broad sense of PBC, but if we're talking about undecidability, this would, if I'm not mistaken, always be a proof of negation. After marinating for a couple of days I realized this answer is wrong, although it is onto something. Though I think I had a point, I think it's also more confusing than it is useful, and should probably be ignored. I'm not sure of the etiquette of dealing with wrong answers, so I'll leave it as-is with a note. $\endgroup$
    – Eilene FTF
    Sep 13 at 15:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.