How to decompose A if and only if B? I've read that the formula A if and only if B is a formulation of the equivalence
that can be decomposed in A if B (the implication B -> A) and in A only if B (the implication A -> B). 
I don't agree with the second part : for me it looks like that A only if B is the translation of ¬B -> ¬A (I know that it's the contraposition of A -> B and consequently it means the same but it's not the same formulation).
So can anyone tell me the correct interpretation please.
thanks,
Bruno
 A: If I understand your question correctly, you are bothered by the semantics of the statement "$A$ only if $B$".  You can take this statement as idiomatic, that is, if taken literally it has one meaning, but social convention (in this case the social convention of the mathematics community) leads us to interpret it as always meaning $A \rightarrow B$.  There is certainly room in English to take certain phrases as being somewhat illogical.  My point is that "$A$ only if $B$" doesn't actually have to stand up to logical dissection of the semantics.  Extracting meaning from English sentences is not linear.
However, I always look at that the statement "$A$ only if $B$" as meaning A is true only if B is true.  If we look at a truth table for a statement where A is true only if B is true, then we see that this is equivalent to the statement $A\rightarrow B$. 
A: I am not sure I am understanding what you are asking, so my answer my not address what you are asking.
For an if an only if (iff) theorem, you have $A \Leftrightarrow B$. This means that A only occurs when B occurs and B only occurs when A occurs. If you are trying to prove an iff theorem, you must prove it in both directions. That is, you must show that $A \Rightarrow B$ and then show that $B \Rightarrow B$.
A: I would expand "A only if B" to "A can only be true if B is also true", then go to "if A then B" and represent that as $A \implies B$.  As you say, that is English processing, not logic processing.
A: In classical logic, $B\rightarrow A$ is equivalent to $\lnot A \rightarrow \lnot B$, so you will simply use the simplest definition of $A\leftrightarrow B$, which is to use $B\rightarrow A$. In intuitionistic logic, the contraposition is not generally derivable. You have $(B\rightarrow A)\rightarrow(\lnot A\rightarrow \lnot B)$, but not $(\lnot A\rightarrow \lnot B)\rightarrow(B\rightarrow A)$. Hence, your definition of equivalence is weaker - and doesnt really make sense, it only makes sense if you assume $A\vee \lnot A$.
And if you look at it computationally, $A\leftrightarrow B$ means you have terms $u^{A\rightarrow B}$, $v^{B\rightarrow A}$, such that if you have an object $a^A$ you always get an object $b^B$ and vice versa. With your definition, you would have $u^{A\rightarrow B}$, but $v^{(A\rightarrow\bot)\rightarrow(B\rightarrow\bot)}$ where $\lnot A = A\rightarrow\bot$ and $\bot$ can be defined as $0=1$ (or any other type of which no term is derivable), hence, $v$ maps terms $t^{A\rightarrow\bot}$ that map terms of type $A$ on something not derivable onto terms $u^{B\rightarrow\bot}$ mapping terms of type $B$ on something not derivable.
This isnt what we usually want from equivalence.
