Solving a Smullyan style knight and knave problem using natural deduction. How to shorten this proof?
Here's a proof I made on http://proofs.openlogicproject.org/ Mine is 13 statements versus your 39 (since your proof didn't go to my statement 14). On the other hand, I stuck with a bidirectional formulation and I gather different systems do different things with $\leftrightarrow$E. Still, make of this what you will.
First, I would symbolize the given information as:
$[J \leftrightarrow (~\neg J \leftrightarrow \neg B)] \land [B \leftrightarrow \neg (B \leftrightarrow J)]$
Then, there are some handy-dandy equivalence principles for the biconditional:
Biconditional Commutation
$P \leftrightarrow Q \Leftrightarrow Q \leftrightarrow P$
Biconditional Association
$P \leftrightarrow (Q \leftrightarrow R) \Leftrightarrow (P \leftrightarrow Q) \leftrightarrow R$
Biconditional Negation
$\neg (P \leftrightarrow Q) \Leftrightarrow \neg P \leftrightarrow Q$
$\neg (P \leftrightarrow Q) \Leftrightarrow P \leftrightarrow \neg Q$
$\neg P \leftrightarrow \neg Q \Leftrightarrow P \leftrightarrow Q$
Biconditional Complement
$P \leftrightarrow P \Leftrightarrow \top$
$P \leftrightarrow \neg P \Leftrightarrow \bot$
$P \leftrightarrow \top \Leftrightarrow P$
$P \leftrightarrow \bot \Leftrightarrow \neg P$
With those:
\begin{array}{lll} 1. & [J \leftrightarrow (~\neg J \leftrightarrow \neg B)] \land [B \leftrightarrow \neg (B \leftrightarrow J)] & Given\\ 2. & [J \leftrightarrow (~\neg J \leftrightarrow \neg B)] \land [B \leftrightarrow (\neg B \leftrightarrow J)] & Biconditional \ Negation \ 1\\ 3. & [(J \leftrightarrow ~\neg J) \leftrightarrow \neg B] \land [(B \leftrightarrow \neg B) \leftrightarrow J] & Biconditional \ Association \ 2\\ 4. & [\bot \leftrightarrow \neg B] \land [(\bot \leftrightarrow J] & Biconditional \ Complement \ 3\\ 5. & B \land \neg J & Biconditional \ Complement \ 4\\ \end{array}
Also notice that a reasonable symbolization of Bill's statement would have been $B \leftrightarrow (\neg B \leftrightarrow J)$, in which case I could have started on line 2, and obtained the result in a mere $3$ inference steps.
EDIT: following a suggestion by Matt Daly:
Let's suppose we also have:
Biconditional Substitution
$S(P) \land (P \leftrightarrow Q) \Leftrightarrow S(Q) \land (P \leftrightarrow Q)$
where $S(Q)$ is the result of replacing any occurrence of $P$ with $Q$ in $S(P)$
Biconditional Reduction
$P \land (P \leftrightarrow Q) \Leftrightarrow P \land Q$
$\neg P \land (P \leftrightarrow Q) \Leftrightarrow \neg P \land \neg Q$
and symbolizing Bill's statement as $\neg (J \leftrightarrow B)$, we get:
\begin{array}{lll} 1. & [J \leftrightarrow (\neg J \leftrightarrow \neg B)] \land [B \leftrightarrow \neg (J \leftrightarrow B)] & Given\\ 2. & [J \leftrightarrow \neg (J \leftrightarrow \neg B)] \land [B \leftrightarrow (J \leftrightarrow \neg B)] & Biconditional \ Negation \ 1\\ 3. & [J \leftrightarrow \neg B] \land [B \leftrightarrow (J \leftrightarrow \neg B)] & Biconditional \ Substitution \ 2\\ 4. & [J \leftrightarrow \neg B] \land B & Biconditional \ Reduction \ 3\\ 5. & \neg J \land B & Biconditional \ Reduction \ 4\\ \end{array}