Express $(A\to B)\land((C\land B)\to A)$ using biconditional

Question

Is there a way to express the formula $(A\to B)\land((C\land B)\to A)$ as a biconditional, i.e. as a statement of the form $\phi\leftrightarrow\psi$ for some expressions $\phi(A,C)$, $\psi(B,C)$? Of course one could always set $\psi=\top$ and $\phi=(A\to B)\land((C\land B)\to A)$ but I want something a little less trivial, hence the restriction that $B$ not be present in $\phi$ and $A$ not in $\psi$ (which I will readily relax if there is some other reasonable nontrivial solution). The obvious first attempts are $(C\land A)\leftrightarrow(C\land B)$, which only gives $(C\land A)\to B$ for the forward implication, and $A\leftrightarrow(C\land B)$, which also gives $A\to C$ in the reverse implication.

Answer 1

$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\calcop}[2]{\\ #1 \quad & \quad \unicode{x201c}\text{#2}\unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\followsfrom}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}} $I can't find anything that matches your requirements exactly, but does perhaps $$\tag 0 (C \then A) \;\equiv\; (A \then B) \land (C \then B)$$ fit your bill?

I found this by putting (A => B) && ((C && B) => A) into Wolfram Alpha, which suggested as one minimal form the DNF $$\tag 1 (A \land B) \lor (\lnot A \land \lnot B) \lor (\lnot A \land \lnot C)$$ which readily transforms into the above expression:

$$\calc \tag 1 (A \land B) \lor (\lnot A \land \lnot B) \lor (\lnot A \land \lnot C) \calcop={basic property of $\;\equiv\;$} (A \equiv B) \lor (\lnot A \land \lnot C) \calcop={$\;\lor\;$ distributes over $\;\equiv\;$} A \lor (\lnot A \land \lnot C) \;\equiv\; B \lor (\lnot A \land \lnot C) \calcop={simplify LHS} \tag{*} A \lor \lnot C \;\equiv\; B \lor (\lnot A \land \lnot C) \calcop={distribute $\;\lor\;$ over $\;\land\;$ in RHS; introduce $\;\then\;$, three times} \tag 0 (C \then A) \;\equiv\; (A \then B) \land (C \then B) \endcalc$$

This is the most 'symmetrical' form that I've been able to find: but I've only been doing this by trial and error. The shortest form I could find is $\ref *$, or its DeMorgan variant $\;A \lor \lnot C \;\equiv\; B \lor \lnot (A \lor C)\;$.