# 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?

• Well it's always both. – Kenny Lau Sep 23 '17 at 6:22
• $A \iff B$ is defined as $A \to B \land B \to A$, right? – Kenny Lau Sep 23 '17 at 6:26
• @KennyLau Classical logic has different rules than constructive logic. – DanielV Sep 23 '17 at 6:47
• Then how is $A \iff B$ defined? – Kenny Lau Sep 23 '17 at 7:08
• @KennyLau That's how $A\iff B$ is defined, but the question is about situations like, for example, $\varphi\iff\neg\neg\varphi$ which is provable classically but only $\varphi\implies\neg\neg\varphi$ is provable constructively. – Derek Elkins Sep 23 '17 at 7:33

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