What does it mean to suspect that two conjectures are logically equivalent?

First of all, in practice when we say "Conjecture A is equivalent to Conjecture B," what we mean is "We have a proof that Conjecture A is true iff Conjecture B is true." We can have such a proof without having a proof of either conjecture, so this is a meaningful situation. Of course, it will (hopefully) later become trivial, when we prove or disprove the conjectures (and so reduce it to "they're both true" or "they're both false").

But your question has more to it than that: suppose we want to say that two theorems we already know to be true are equivalent. How can we do that? (Note that this is something we in fact do all the time - e.g. when we say "the compactness of the real numbers is equivalent to their satisfying the extreme value theorem.")

The simplest approach to this is by considering extremely weak axiom systems, which aren't strong enough to prove either result but can prove the equivalence. That is, we work over some very weak "base theory."

Historically, of course, the most well-known example is the study of equivalences/implications between versions of the axiom of choice over the theory ZF; as a fun fact, there's a famous story that when Tarski tried to publish a certain equivalence over ZF, one editor rejected it on the grounds that the equivalence between two true statements isn't interesting and the other rejected it on the grounds that the equivalence between two false statements isn't interesting. (I believe there were also hints of interest in equivalences between true principles in the study of absolute geometry, but I'm not certain - it's been a while since I looked at the history of non-Euclidean geometry.) However, ZF is "too strong" for most statements of mathematical interest, so we want to go deeper into things.

This is one of the motivations behind reverse mathematics: we look at equivalences/implications/nonimplications over a very weak theory, RCA$_0$, which intuitively corresponds to "computable" mathematics with "finitistic" induction only.

For example, here are some statements which are all equivalent to each other in the sense of reverse mathematics:

  • Every commutative ring which is not a field or the zero ring has a nontrivial proper ideal.

  • $[0,1]$ is compact.

  • Every infinite binary tree has an infinite path.

(There is actually a serious issue here which doesn't really crop up when proving equivalences over ZF, namely that we have to figure out how to express the statements we care about in the language of our base theory; this is an issue with weak theories like RCA$_0$ whose language is quite limited. I'm ignoring this issue completely here.)

And we sometimes want to go weaker still. Equivalences over theories much weaker than RCA$_0$ have been studied, albeit not (in my understanding) as extensively.


Noah Schweber's answer is in some sense the "right" answer, and I would have said something similar if he hadn't beaten me to it. However, I think that it's worth pointing out that reverse mathematics isn't necessarily the end of the story.

The Wikipedia entry on Sperner's lemma says (as of this writing):

In mathematics, Sperner's lemma is a combinatorial analog of the Brouwer fixed point theorem, which is equivalent to it.

Notice the word "equivalent." In my opinion, Wikipedia is correct, and in the minds of most mathematicians who understand both Sperner's lemma and Brouwer's fixed-point theorem, the two results are equivalent in the sense that proving one from the other is relatively straightforward, whereas proving either one of them from scratch requires a nontrivial idea. Moreover, in some sense it's the same nontrivial idea that you need in either case.

However, if you look at the reverse mathematics literature, you'll find that Sperner's lemma is provable in the base system RCA0 whereas Brouwer's fixed-point theorem isn't. In fact, it's a standard result in reverse mathematics that Brouwer's fixed-point theorem is equivalent to the Weak Koenig Lemma and hence belongs naturally in the system WKL0, which is stronger than RCA0.

What's going on? Roughly speaking, in order to pass from Sperner's lemma to Brouwer's fixed-point theorem, you need to pass to a limit in a certain way, or apply mathematical induction to a certain class of propositions, and to do this is to invoke a logical principle that isn't needed in most of mathematics (and hence has been omitted from RCA0). This is a perfectly reasonable thing to do when setting up systems for reverse mathematics. However, what one has to keep in mind is that logical strength is not the same as psychological difficulty. Somehow, for most humans, the clever idea needed to prove Sperner's lemma is harder to hit upon than the "limiting process" that is needed to pass from Sperner's lemma to Brouwer's fixed-point theorem.

What this means is that reverse mathematics, at least as it is standardly constructed, is not currently in a position to provide a rigorous logical basis for the intuition that Sperner's lemma is equivalent to Brouwer's fixed-point theorem. What is probably needed is a precise theory of inferences that are easy for humans to see. Then we could define $P\implies Q$ to mean that $Q$ is "easily inferred" from $P$. Equivalence would mean that $P\implies Q$ and $Q\implies P$ but neither $P$ nor $Q$ is "easily inferred" from some standard base theory. As you can see when I put it this way, there is probably no canonical way to construct such a theory, and even if one succeeds in coming up with a plausible candidate, it is going to have some counterintuitive properties. For example we won't always be able to conclude from $P\implies Q$ and $Q\implies R$ that $P\implies R$ (otherwise every theorem would be "easy to prove").


One way to say rigorously what it means for two true theorems to be equivalent is to find a meaningful way to generalize both of them to statements that aren't always true, and then prove that they're true in the same situations. For example:

Observe that the fundamental theorem of algebra is equivalent to $0 = 0$, but in a trivial sense since they are both true.

But of course there is a natural generalization of the fundamental theorem of algebra to a statement that isn't always true: namely, the claim that some field is algebraically closed.

Here is another simple example. One might ask, "is the statement that $\mathbb{Z}$ has a division algorithm equivalent to the statement that numbers have unique prime factorizations?" A priori it's unclear what this means since both statements are true. But again they both have natural generalizations: namely, to the claim that some commutative ring is a Euclidean domain vs. the claim that it's a UFD. And at this level of generality we know that Euclidean implies UFD but that there are UFDs that aren't Euclidean.

This is maybe not an answer to your question as stated since I replace the original two statements $p$ and $q$ with some other statements, but I think examples of this phenomenon occur frequently enough that it's worth pointing out explicitly. If I were to say, "the division algorithm is a strictly stronger statement than unique prime factorization," even though I'm talking about the integers what I mean is this general fact that Euclidean domains are UFDs but not conversely.