What is the minimal complexity formula equivalent to biconditional?

Question

Suppose we are working in the propositional language whose only primitive logical connectives are $\rightarrow$ and $\neg$, standing for conditional and negation, respectively. Disjunction can be defined as $\neg A \rightarrow B$, conjunction can be defined as $\neg(A \rightarrow \neg B)$, and biconditional can be defined as $(A \rightarrow B) \land (B \rightarrow A)$. Unabbreviating the last one, biconditonal, we get $\neg((A \rightarrow B) \rightarrow \neg(B \rightarrow A))$. My question is, is that a formula of minimal complexity which is equivalent to biconditional? Or is there some simpler formula in terms of conditional and negation which is equivalent to biconditional?

Answer 1

It's easy to see that three $\rightarrow$s are needed (irrespective of how many $\neg$s are used). Any expression $\psi(A,B)$ with two $\rightarrow$s has (perhaps after some double-negation-elimination) one of the following four forms $$\varphi\rightarrow C,\quad \varphi\rightarrow\neg C,\quad C\rightarrow\varphi,\quad \neg C\rightarrow \varphi$$ for $C\in\{A,B\}$. In the first and fourth cases $\psi$ is true if $C$ is true, and in the second and third cases $\psi$ is true if $C$ is false. Either way, the truth of $\psi$ can be ensured simply by an appropriate choice of truth value for one of the constituent atoms, and this is not the case for bi-implication.

In fact, what the above really shows is that any expression for bi-implication must have one of the forms $\varphi\rightarrow\theta$ or $\neg(\varphi\rightarrow\theta)$ for some $\varphi,\theta$ not $\rightarrow$-free. A bit of casework then shows that two negations are necessary if you want the "implication diagram" of $\psi$ to be as simple as possible, namely $$(?\rightarrow ?)\rightarrow(?\rightarrow?).$$ This does leave some wiggle-room (can you use fewer negations with more implications?) but I think it's overall pretty compelling.