Constructive logic vs classic logic for $\vdash A \iff B$ Is it always the case that if $\emptyset \vdash A \iff B$ in classical logic then at least one of $\emptyset \vdash A \to B$ or $\emptyset \vdash B \to A$ in constructive logic?  Does it depend on if you are restricted to propositional logic vs predicate logic?
 A: The answer is "no" even in intuitionistic propositional logic, which is what I assume you mean by "constructive logic".
$
\def\imp{\Rightarrow}
\def\eq{\Leftrightarrow}
\def\from{\leftarrow}
$
Let $P \overset{def}\equiv ( A \lor \neg A ) \eq ( B \lor \neg B )$. Then $P$ is a classical tautology. But let $K$ be a Kripke frame with worlds $0 \to 1$ and $2 \to 3$ where $A$ holds at only $1$ while $B$ holds at only $3$. Then the implication $( A \lor \neg A ) \imp ( B \lor \neg B )$ is false in $K$ because at $2$ we have that $\neg A$ (which denotes "$A \to \bot$") holds but neither $B$ nor $\neg B$ hold. By symmetry, $( B \lor \neg B ) \imp ( A \lor \neg A )$ is false in $K$ too. Thus for atoms $A,B$ neither of the implications be proven.
A: For a somewhat different example, let $P$ and $Q$ be propositional variables. Then intuitionistic propositional logic does not prove $(P \land \lnot\lnot Q) \to (\lnot\lnot P \land Q)$ (and hence, by symmetry, it does not prove $(Q \land \lnot\lnot P) \to (\lnot\lnot Q \land P)$). To see this note that if intuitionistic logic could prove $(P \land \lnot\lnot Q) \to (\lnot\lnot P \land Q)$, it could also prove $(\top \land \lnot\lnot Q) \to (\lnot\lnot \top \land Q)$, which it can prove equivalent to the law of double negation elimination, $\lnot\lnot Q \to Q$, which is not intuitionistically valid.
