Biconditional statements with an "easy" direction.

I was reading through Lax's Functional Analysis, when I came across the following statement:

Theorem: X is a normed linear space over $\mathbb{R}$, $M$ a bounded subset of $X$. A point $z$ of $X$ belongs to the closed, convex hull $\breve{M}$ of $M$ iff for all $l$ in $X'$, $$l(z) \leq S_M(l).$$

I don't have a question about this theorem, but I would like to use it as an example. Its proof, like many "if and only if" proofs has one direction (the forward one in this case) which is fairly trivial and one that is difficult. This is reflected in the length of the two parts of Lax's proof. I'm sure there are much better examples than this.

After reading this theorem, I was reminded of a professor I had not too long ago who made a big deal about these asymmetrical proofs. I remember he asked us, "If two statements are equivalent, why shouldn't it be equally easy to prove one from the other?" He admitted he had no real answer, but suggested it had to do with human psychology. Other people I've spoken to have claimed that, to some great genius, both directions would be of equal difficulty.

My questions are these:

1. Is this actually an interesting phenomenon?
2. If it is, is there any way to state it less "softly?"
3. Do you have any favorite examples of these theorems?
4. Why is one direction easier in these cases?

Thanks and hope this isn't too vague.

I would not step to the esoteric or psychological level here. Let me introduce an easy example of two obviously equivalent statements: $\forall x Rx$ holds if and only if $(\exists x Px \lor \forall x\neg Px)\rightarrow \forall x Rx$, so $$\forall x Rx \leftrightarrow((\exists x Px \lor \forall x\neg Px)\rightarrow \forall x Rx)$$ is a tautology. But see what happens if we prove the two directions in a sequent calculus:

Direction "$\rightarrow$"

Direction "$\leftarrow$"

The essence of the example: Just because two formulas $\varphi$ and $\psi$ are equivalent, this does not mean that the proofs of the logical true, but otherwise potentially substantially different formulas $\varphi\rightarrow\psi$ and $\psi\rightarrow\varphi$ are equally hard. In the example, we had to actually proof the premise $\exists x Px \lor \forall x\neg Px$ in the "$\leftarrow$" direction, while we could treat it in the "$\rightarrow$" direction as a blackbox.

Also: The logical equivalence of two formulas tells us nothing about the complexity of their respective proofs! This is no human psychology, just technical issues. And a genius would probably look at the formulas and state: "hey, but the second one will have a more complex proof" ;)

Remark: I you are not comfortable with the sequent calculus, regard it the following way: In the left-to-right direction, you can exploit the fact that $\varphi\rightarrow(\psi\rightarrow\varphi)$ is always true (propositional tautology), regardless of the truth of $\psi$. For $(\psi\rightarrow\varphi)\rightarrow\varphi$, you have to prove $\psi$ first, because only then this becomes logically true. All this is not effected by the fact that the formulas of the above example are equivalent, and both directions are therefore provable. Provability and complexity of proofs are two different things.

1. Is this actually an interesting phenomenon?

I'd vote for yes - but rather from the proof-theoretic "technical" point of view than from a philosophical one.

1. If it is, is there any way to state it less "softly?"

Well, you could phrase it towards an investigation of the lengths of the shortest proofs (in a formal system) for the two directions of a bi-implication.

1. Do you have any favorite examples of these theorems?

One of my favorites is the soundness and completeness of a formal proof system for first-order logic: A theorem is logically true if and only if it is provable in the system.

1. Why is one direction easier in these cases?

The "$\leftarrow$" direction (soundness) is the easy one, you just have to do a structural induction over the calculus. The "$\rightarrow$" direction ((strong) completeness) is the complicated (and more interesting) one; interesting facts like the compactness theorem follow from the existence of such complete proof systems.

I think a lot of theorems could be stated in such a way as to fulfil the requirements, e.g., $x^n+y^n=z^n$ has a solution in positive integers if and only if $n\le2$; the Riemann zeta function has infinitely many zeros with real part $s$ if and only if $s=1/2$ (OK, the "only if" part may not be a theorem just yet); there is a sporadic simple group of order $n$ if and only if $n$ is in the following list [insert here list of orders of sporadic simple groups], and so on. Perhaps a more interesting example is Hall's Marriage Theorem, which gives a necessary and sufficient condition for the existence of certain pairings. The "necessary" part is trivial, the "sufficient" part takes a bit of work.