I want to write a propositional logic formula for the biconditional that only uses one side of the biconditional once in the formula. I expect it is impossible, but can anyone think of a proof? There are many formulas for the biconditional:
\begin{align}P\leftrightarrow Q&\equiv(P\to Q)\wedge(Q\to P)\\ &\equiv(P\vee Q)\to(P\wedge Q)\\ &\equiv(P\wedge Q)\vee(\neg P\wedge\neg Q)\\ &\equiv(P\vee Q)\wedge(\neg P\vee\neg Q) \end{align}
but all of these use both $P$ and $Q$ twice. (I allow $\wedge,\vee$ in the above because they can both be written in terms of $\to,\neg$ without any extra duplication of the variables: $$P\vee Q\equiv\neg P\to Q,\quad P\wedge Q\equiv\neg(P\to\neg Q).$$
Similarly, NAND and NOR can be expressed using the variables only once, but XOR can be so expressed iff the biconditional can, and that's the question. It is okay if one of the variables has to be duplicated, as long as the other one appears only once.
If there exist such formula, it must be like this: $$f(P,Q)\to g(Q)$$ where $P$ appears once in $f$, and, since it is equivalent to $P\leftrightarrow Q$, we have $$\begin{align} f(0,0)&\to g(0)\\ f(0,1)&\wedge\neg g(1)\\ f(1,0)&\wedge\neg g(0)\\ f(1,1)&\to g(1) \end{align}$$
The 2nd and the 3rd formulas imply that $g(0)=g(1)=0$, that is, $g(Q)\equiv Q\wedge\neg Q$. Then $f(P,Q)\equiv \neg(P\leftrightarrow Q)$, so the formula $\neg f(P,Q)$ is a shorter one that verify the condition. That is, every formula that verifies the condition can be shortened.
This is a contradiction, so the formula that you are looking for doesn't exist.