9
$\begingroup$

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?

Improve this question
$\endgroup$
9
  • $\begingroup$ If users think this question is not formulated precisely enough, or belongs to another forum, then I'm happy to delete or move it. $\endgroup$
    – Ian Agol
    Commented May 17, 2014 at 19:41
  • $\begingroup$ 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))$ $\endgroup$
    – Christian Remling
    Commented May 17, 2014 at 19:50
  • $\begingroup$ 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. $\endgroup$
    – Ryan Budney
    Commented May 17, 2014 at 19:51
  • $\begingroup$ Not a fascinating example, but "a square matrix is invertible iff it has nonzero determinant" seems like an example. $\endgroup$
    – François G. Dorais
    Commented May 17, 2014 at 20:06
  • $\begingroup$ 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. $\endgroup$
    – Carl Mummert
    Commented May 17, 2014 at 21:03

2 Answers 2

Reset to default
9
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented May 17, 2014 at 20:29
  • $\begingroup$ Ok, I thought there might be a more non-trivial example, which didn't just follow from the existence of arbitrarily long proofs. $\endgroup$
    – Ian Agol
    Commented May 18, 2014 at 16:39
  • $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented May 18, 2014 at 22:18
10
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – Ian Agol
    Commented May 18, 2014 at 1:16
  • $\begingroup$ @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. $\endgroup$
    – Lawrence Wong
    Commented May 18, 2014 at 8:48
  • $\begingroup$ @LawrenceWong I don't think that applies to my example though? $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented May 18, 2014 at 15:29
  • $\begingroup$ @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$". $\endgroup$
    – Lawrence Wong
    Commented May 18, 2014 at 18:48
  • $\begingroup$ @LawrenceWong oh I see $\endgroup$
    – Bjørn Kjos-Hanssen
    Commented May 18, 2014 at 19:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .