Here's a familiar conversation:

Me: Do you think Conjecture A and Conjecture B are equivalent?

Friend: Yes, because I think they're both true.

Me: [eye roll] You know what I mean...

Does there exist a rigorous notion of what I mean? Perhaps something about the existence of a proof of $p \Leftrightarrow q$ that doesn't "come close" to revealing the truth value of either $p$ or $q$? Unfortunately, the idea of "coming close" sounds rather subjective and reminiscent of Timothy Chow's answer here. Perhaps there's another approach?

Edit: Judging by the immediate response, it seems that my question requires additional clarification. I am wondering whether there is a rigorous notion in logic for pairs of statements that are logically equivalent in a nontrivial sense. Observe that the fundamental theorem of algebra is equivalent to $0=0$, but in a trivial sense since they are both true. On the other hand, one might consider $p\Leftrightarrow q$ to be "nontrivially true" if there exists a proof of $p\Leftrightarrow q$ despite $p$ not being provable. Is there a more general theory that applies in the case where $p$ is provable?

  • 1
    $\begingroup$ Related: Proof complexity of two directions of equivalency? $\endgroup$
    – jeq
    Oct 23 '17 at 19:36
  • 13
    $\begingroup$ In a practical sense, when we say that $p$ implies $q$ where $p$ and $q$ are theorems, what we mean is that a proof of $q$ from $p$ is "significantly simpler" and/or "significantly shorter" than a proof of $q$ from scratch. This could be made rigorous by comparing the length of the shortest proof of $p⇒q$ to that of $q$ alone, although I'm not sure it's really an interesting formalization, but it undoubtedly makes sense. $\endgroup$
    – Gro-Tsen
    Oct 23 '17 at 21:41
  • 3
    $\begingroup$ Timothy Gowers has a blog post on a related topic: gowers.wordpress.com/2008/12/28/… $\endgroup$ Oct 23 '17 at 22:32
  • 3
    $\begingroup$ Well, there are fields where the fundamental theorem of algebra does not hold, replacing "complex numbers" with the appropriate field (like the field of reals) and it would still be the case that $0=0$. That makes it seem like those two statements are not equivalent. Maybe it depends on what sort of generalizations you accept in the particular context you're working in. $\endgroup$
    – David
    Oct 24 '17 at 2:21
  • 2
    $\begingroup$ To repeat a comment I made on Gowers' post linked above: one informal way to measure the extent to which two already proven conjectures A and B are equivalent is to imagine if someone published a proof of a variant A' of Conjecture A, and to see to what extent one would then expect there to soon be progress on some variant B' of Conjecture B, and vice versa. (Many of the answers below can be viewed in this framework, where A' is obtained by A by varying the axiom system, some parameters, etc.. One could also consider qualitiative vs quantitative variants, discrete vs continuous, etc..) $\endgroup$
    – Terry Tao
    Oct 24 '17 at 17:39

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.

  • 14
    $\begingroup$ @PaceNielsen RCA$_0$ is really weak - it corresponds to computable mathematics, and computability is a seriously strict condition! RCA$_0$ doesn't know that $xR$ exists: $xR$ is defined in a non-computable way (to tell that $y\not\in xR$, we have to search through all $z\in R$). In fact, "$xR$ always exists" is equivalent to ACA$_0$! See this paper. $\endgroup$ Oct 24 '17 at 4:23
  • 2
    $\begingroup$ Very interesting, +1! One small quibble: do you mean "completeness of the real numbers", as opposed to compactness? $\endgroup$ Oct 26 '17 at 23:01
  • 1
    $\begingroup$ Relevant to the concept of reverse mathematics, I highly recommend James Propp's article from the American Mathematical Monthly entitled "Real Analysis in Reverse": arxiv.org/abs/1204.4483 $\endgroup$ May 4 '18 at 23:18
  • 1
    $\begingroup$ woah!!! (+1) I find the commutative ring example here really mindblowing, somehow it "feels" much weaker to me than the other statements. do you have any recommendations for a (brief) introduction to reverse mathematics? $\endgroup$
    – user147820
    Mar 24 '21 at 14:59
  • 2
    $\begingroup$ @AtticusStonestrom I learned reverse math by starting with the paper Ideals in computable rings and alongside that reading the first bit of Subsystems of second-order arithmetic. The latter is more useful as a reference than a self-study text, but the first chapter is an exception to this, and is a good brief introduction. There's also a more recent book Slicing the truth, but I haven't actually worked with it in detail. $\endgroup$ Mar 24 '21 at 15:02

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

  • 6
    $\begingroup$ Neat, I didn't know this! A minor quibble, though: "... or apply mathematical induction to a certain class of propositions ..." suggests that the problem is that RCA$_0$ doesn't have enough induction. But WKL$_0$ doesn't have any more induction than RCA$_0$ does (in a precise sense: WKL$_0$ is $\Pi^1_1$-conservative over RCA$_0$). While RCA$_0$ does restrict the amount of induction that's allowed, and this is an issue with many results (e.g. finite Ramsey's theorem), that's not what's going on here. (Also, worth linking - Francois Dorais' answer here.) $\endgroup$ Oct 24 '17 at 3:09
  • $\begingroup$ @NoahSchweber : Yes, you're right, I was careless. But I'll leave my answer as it stands since editing my answer would make your excellent comment less intelligible. $\endgroup$ Oct 24 '17 at 3:20
  • 2
    $\begingroup$ @QiaochuYuan Yes, if I recall correctly. My understanding is that we get to Brouwer from Sperner via an appropriate compactness argument; but compactness arguments in general are beyond RCA$_0$ (they tend to correspond to WKL$_0$). So Sperner=Brouwer if one is willing to assume such compactness arguments as "basic." (I $\endgroup$ Oct 24 '17 at 12:19
  • 3
    $\begingroup$ @TimothyChow: I would say that one way is to define the difficulty of a theorem to be the length of its shortest proof over the mathematicians' preferred formal system. Then it may be that two theorems both have high difficulty but the equivalence has low difficulty, hence if we want to prove both then in some sense all we need to do is prove one and tack on the (short) equivalence proof to get the other as well. $\endgroup$
    – user21820
    Oct 24 '17 at 15:46
  • 5
    $\begingroup$ @user21820 : Proof length is certainly a tempting way to measure psychological difficulty, and may be the simplest way to make these ideas rigorous. On the other hand, there are many examples that demonstrate that "short proof" isn't necessarily the same as "easy proof." In fact, I suspect that for most theorems that have two or more known proofs that are recognizably distinct, the shorter proof is not the one that was first discovered, whereas the first proof is probably, in most cases, easier to find. $\endgroup$ Oct 24 '17 at 22:27

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.

  • 1
    $\begingroup$ And this answer generalizes the weak axiom system answer, which generalizes by claiming the conjectures over more axiom systems. $\endgroup$ Oct 24 '17 at 16:01

As has been said Timothy Chow's answer and the comments, what mathematicians really mean when they use "equivalent" in this setting is that it's easy to prove the equivalence. That's not the same as the logical strength, and it's not the same as the number of steps. What it means is more like "how much time would it take for an undergrad/grad/expert to understand/find this proof of equivalence." (Of course each of those six possibilities are different and though they have an obvious partial ordering by strength there's not a clear linear ordering.)

Now one might object that these definitions are somewhat imprecise mathematically, but what I want to argue is that they're likely quite precise practically. We all know that there's relatively clear line between an exercise that we can expect all the students in a grad class to solve, an exercise we can expect them to solve with a particular hint, and one only a few people will solve. If we brought in different groups of graduate students to a lab, I'd be pretty confident that there'd be clear level of difficulty for most problems.

If you don't like people as a measurement here, then relatively soon you'll be able to sub out people for AIs and get a more objective (though less accurate) measurement of what mathematicians mean here. For example, the Ganesalingam-Gowers AI for proving results in metric space topology gives a pretty clean definition of the undergrad/find case of the above definition for statements about metric spaces. Two conjectures are undergrad/find equivalent if the Ganesalingam-Gowers AI can prove that the statements are equivalent but can't prove either one. As far as I can tell we don't yet have good AIs to model the other five definitions.

Makes me wonder whether there's a good example of statements about metric spaces that are both true but which are Ganesalingam-Gowers equivalent but not Ganesalingam-Gowers provable.

  • 2
    $\begingroup$ I don't agree that that line is so clear. I have often been surprised in both directions. $\endgroup$ Nov 18 '17 at 12:51

A pure logic approach:

On the other hand, one might consider p⇔q to be "nontrivially true" if there exists a proof of p⇔q despite p not being provable.

Provability of the individual statements, or their truth value, are both irrelevant for equivalency. The logic goes the other way: if p is provable, and you don't know about the provability of q yet, and then you discover that p is equivalent to q, you hereby have proven q.

Is there a more general theory that applies in the case where p is provable?

Well, that theory is called "logic" (you could look into predicate logic, lambda calculus and such if you require more specific and rigorous information). It is very much about about definitions as well. p being equivalent to q is defined as "p implies q and q implies p". This applies to mathematical proofs as well as algorithms or (abstract) computer programs, regarding decidability, computability, complexity and such. Since Gödel et al, maths and CS are really on the same page, here.

In fact, in computer science, creating sets of problems based on deducing one from the other (without knowing much or, in some cases, anything at all about either) is one of the most basic techniques that is applied all the time.


Me: [eye roll] You know what I mean...

Even so it may seem like "Noah Schweber's answer is in some sense the 'right' answer", it actually fails completely to address the [eye roll]. The normal mathematician in the street doesn't think about equivalences over week theories of reverse mathematics when he talks about two conjectures being equivalent. So it is unlikely that he meant such equivalences, especially since the material implication is known to be incompatible with the validity of logical implication in natural language.

Noah Snyder and Qiaochu Yuan's answers are much closer to what a normal mathematician means, when he talks about equivalences.

But even if one wants to interpret equivalence with respect to formal systems, the assumption that the two conjectures and the proof of their equivalence live in the same formal system is not always justified. A common situation is that one of the conjecture lives in a very weak formal system, the other conjecture lives in normal informal mathematics, and the proof of their equivalence will be done either informal, or in an arbitrary sufficiently powerful formal system (like ZFC). For example, the Goldbach conjecture is equivalent to a $\Pi_1^0$ statement, i.e. a sentence asserting that some given Turing machine never halts at the empty input tape. The point of such an equivalence is to highlight that the conjecture being true or false has some very real computational content, instead of a potentially merely informal meaning. (I first encountered Noah Schweber's suggestion that weak systems of reverse mathematics would give meaning to equivalences, when I made the guess that the "model existence theorem" would not be equivalent to a $\Pi_1^0$ or $\Pi_2^0$ statement, i.e. lack such a very real computational content.)

(My reason to start writing this answer was another example, which is not exactly a conjecture, but a definition. Sam Sanders uses the Gauge Integral as an example of a definition which cannot be formulated in second order arithmetic. It requires existential quantification over all gauge functions $\delta: [a,b]\to(0,\infty)$ functions, which is a third order object. But I don't like this, and try to prove that if the function $f$ to be integrated is used as a parameter, then quantification over a second order object is sufficient. Here, the definition of the Gauge integral lives in normal informal mathematics, the other definition lives in second order arithmetic (with third order parameters), and the proof of equivalence may live in informal mathematics or ZFC.)


This reminds me of a probably naive attempt in my early twenties (I'll turn 36 soon) to define "deduction nets" as directed multigraphs whose vertices would be propositions and edges "logical links", that is, one has an edge from $ P $ to $ Q $ if one can infer $ Q $ from $ P $ in a single step. The notion of equivalence the OP is seeking is thus a bidirectional edge between the vertices $P$ and $Q$, and "we deduce $C$ from the conjunction of $A$ and $B$" would translate as a kind of Y shape with $A$ and $B$ on the top and $C$ at the bottom thereof. My (naive, once again) idea was that representing a reasoning that way would have made it easier to perform. I never really applied this idea though.

  • 3
    $\begingroup$ Something like this exists in the form of Girard's proof nets, or in Hughes' combinatorial proofs. I think an important problem with applying these ideas to this question, though, is determining what "a single step" should mean. There are long arguments which seem "content-free" to me, in the sense of not adding to the essential number of steps in some sense. $\endgroup$ Oct 24 '17 at 12:28

It is all about the difference between equivalence and biconditional (ie. implication and conditional). p bic q is true iff p and q have the same truth value (both true or both false), but p equ q is true iff p and q have the same truth value in all possible situations (all possible worlds, in logical parlance). E.g. 0=0 is not equivalent to the fundamental theorem of algebra becouse there are situations in which fta is not true (field of reals) although 0=0 is true in every situation. Another formulation of the difference: a true biconditional is not a valid biconditional (which is equivalece).

  • $\begingroup$ I think you should use your other identity if you want to edit. $\endgroup$ Jul 19 '19 at 12:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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