10

This question is not precise, but I believe has a precise formulation.

Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:

Theorem. A compact 3-manifold is simply-connected if and only if it is homeomorphic to the 3-sphere.

The if direction is an exercise in a first course in algebraic topology, and the only if direction is a celebrated result of Perelman.

The question is, are there results which have been shown that one direction of a proof is "harder" than the other?

Certain equivalence proofs seem to have the same complexity in both directions, when all the steps of the proof are reversible.

I think this can be formulated as a precise way, by asking for the length of a proof in a standard proof system. One might also be able to give a precise formulation in terms of the Kolmogorov complexity of a proof.

On the other hand, I can imagine results of the sort that say that for any equivalency, there is a proof system for which one direction is shorter than the other, and another proof system where the reverse holds. So I'm not certain that this question is well-defined. But I think it is well-defined for certain proof systems.

So a more precise question: Is there an equivalence theorem and a proof system, for which it has been shown that one direction of a proof must have a longer proof than the other direction?

Bjørn Kjos-Hanssen
  • 24,629
Ian Agol
  • 66,821
  • If users think this question is not formulated precisely enough, or belongs to another forum, then I'm happy to delete or move it. – Ian Agol May 17 '14 at 19:41
  • If by an equivalence you mean a sentence of the form $A\leftrightarrow B$, then your example is not ideal, because it has the structure $\forall M (A(M)\leftrightarrow B(M))$ – Christian Remling May 17 '14 at 19:50
  • There's aspects of ill-definition that could be concerning. For example, with Perelman's proof, one way to shorten it would be to adjust the axioms. Take the Poincare conjecture as an axiom, and both directions become pretty straightforward. – Ryan Budney May 17 '14 at 19:51
  • Not a fascinating example, but "a square matrix is invertible iff it has nonzero determinant" seems like an example. – François G. Dorais May 17 '14 at 20:06
  • This sort of question comes up very naturally, but it is often hard to find precisely the notion we want to capture. The length of a formal proof is not a very interesting metric, because we don't normally look at formal proofs anyway (so the length is meaningless for practice) and because the length depends as much on the proof system as on the theorem being proved. Reverse Mathematics can capture the set-existence axioms required for each direction. But trying to capture how "easy" or "natural" each direction is to prove is a challenge that has not been solved. – Carl Mummert May 17 '14 at 21:03
  • @ChristianRemling: Actually, a universal quantifier is probably better, to rule out the sort of trivial example in Joel David Hamkins comment to his answer. – Ian Agol May 18 '14 at 01:09
  • It seems to me they still work, after minor modifications (for example $\forall x (x=x \leftrightarrow A(x))$). I think Joel's examples show that no easy formal definition of equivalence captures what you "really" had in mind. – Christian Remling May 18 '14 at 01:19
  • Right, I suppose it's really a metamathematical question, if the mathematical answers are trivial. – Ian Agol May 18 '14 at 01:25
  • The equivalence in ZF of AC and the well-ordering principle should qualify as an example of a statement where one direction is much harder to prove than the other. I don't think it as been shown that the proof of one direction must be much longer / is much harder than the other as is requested in the question. – Joel Adler Oct 22 '17 at 10:53

2 Answers2

10

This fits in the program of reverse mathematics. For instance: a subtree of the set of all finite binary strings has an infinite path iff it is infinite. One direction is provable in RCA $_0$ and the other is not.

Bjørn Kjos-Hanssen
  • 24,629
  • Well, I suppose then that the proof in one direction is definitely "harder" :). But one could probably convert this to such an example, by adding in the appropriate axioms to make it an equivalence, but in a way that would "pad" the proof in the direction that needs them, but not the other. – Ian Agol May 18 '14 at 01:16
  • @Bjørn Kjos-Hanssen: More generally, proving $\forall A\ \exists B\ \Phi(A,B)\rightarrow\exists B\ \forall A\ \Phi(A,B)$ (if it is true for a predicate $\Phi$) is usually harder than proving the converse (which is always true), whatever "hard" means. – Lawrence Wong May 18 '14 at 08:48
  • @LawrenceWong I don't think that applies to my example though? – Bjørn Kjos-Hanssen May 18 '14 at 15:29
  • @BjørnKjos-Hanssen: Perhaps this is a little artificial… The contextual information is that $T$ is a binary tree. Let $A=n$ and $B=P$. The predicate $\Phi(n,P)$ says "$P$ is path through $T$ containing an element of length $n$". – Lawrence Wong May 18 '14 at 18:48
  • @LawrenceWong oh I see – Bjørn Kjos-Hanssen May 18 '14 at 19:32
9

I think that there are numerous trivial examples of this.

Take any implication $p\to q$ that is provable, but has no short proof. It follows that the equivalence $$q\leftrightarrow (p\vee q)$$ is also provable, and furthermore has a trivial proof in the forward direction, but no very short proof in the converse direction, since any such proof also gives a short proof that $p\to q$.

Joel David Hamkins
  • 224,022
  • 2
    Another class of trivial examples: take any provable statement $p$ having no short proof, and consider the equivalence $\top\leftrightarrow p$. Proving the forward implication is just as hard as proving $p$, while the converse implication is immediate. – Joel David Hamkins May 17 '14 at 20:29
  • Ok, I thought there might be a more non-trivial example, which didn't just follow from the existence of arbitrarily long proofs. – Ian Agol May 18 '14 at 16:39
  • Oh, I also expect that there are interesting non-trivial examples. I had just wanted to point out that the phenomenon is much more common than one might have expected, since it also includes all these trivial instances. – Joel David Hamkins May 18 '14 at 22:18