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

Question

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?

Answer 1

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.

Answer 2

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 RCA₀ 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 WKL₀, which is stronger than RCA₀.

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

Answer 3

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.

Answer 4

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.

Answer 5

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.

Answer 6

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

Answer 7

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.

Answer 8

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