Solving a Smullyan style knight and knave problem using natural deduction. How to shorten this proof?

Question

[ EDITED, there were 2 useless lines in the deduction below]

The Smullyan style problem :

John: If (and only if) Bill is a knave, then I am a knave.

Bill: We are of different kinds.

With the understanding that knights only tell true statements and knaves only tell false statements, identify John and Bill's types.

(It therefore follows that if $J$ is the proposition that John is a knight, and John says a logical statement $X$, that $J\leftrightarrow X$ is a tautology.)

My attempt uses natural deduction; but the reasoning is rather long.

Can you think of a shorter natural deduction style proof?

What would be the quickest way to solve the problem according to you?

Below , "J" means " John is a knight" and "B" means " Bill is a knight".

Note: this solution makes Bill's statement true and John's statement false; which is coherent with their being a knight and a knave respectively.

Indeed if we have ( B & ~J) ( that is our alledged solution) John's statement is false, since this statement is equivalent to ( B <-> J) , which, in turn, is equivalent to ~ (B&~J) & ~ ( J&~B).

Answer 1

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.

Answer 2

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}

Answer 3

I know the question was how to shorten your proof, but I think we should first consider whether the proof is valid. It isn't clear to me what axioms or inference rules you're using. For example, "John said: (~B ↔ ~J)" is not a sentence of any formal logic that I know of, and "Knights always tell the truth" isn't an inference rule. You say that J is the proposition that John is a knight, but ~J would then be the proposition that John is not a knight, i.e. that John may lie, which is quite different from the proposition that John always lies.

The answers before mine (Matthew Daly's and Bram28's) have taken J and B to be equivalent to the statements made by John and Bill, which essentially cuts the knighthood/knavehood out of the problem and makes it directly about the truth/falsehood of their statements. That's the easy way to solve the problem.

But since you are putting a lot of work into formalizing the argument as an exercise, you may want to do it the hard way. I haven't thought this through carefully, but you could drop the propositions J and B, and instead introduce formulas JP meaning "John asserts P" and BP meaning "Bill asserts P", and add an axiom like (∀x. Jx → x) ∨ (∀x. Jx → ~x) expressing that John is either a knight or a knave, and a similar axiom for Bill, and formalize their statements as premises J(...) and B(...), and prove (∀x. Jx → ~x) & (∀x. Bx → x). If you want to stick to zeroth-order logic, you could use an axiom schema like (JP ↔ P) ↔ (JQ ↔ Q) to express knight-or-knavehood. Either way, the proof will probably be significantly longer.

Answer 4

I understand that this is not a natural deduction proof, but in response to benrg's comment above, I read somewhere else that you can use algebra in the Galois field of two elements GF(2) to solve things like these, and in that case if you take Z="A is a knave" then you would formalize "A asserts p" as Z + p = 1, since either Z or p are true, but not both . I don't know the details of how to scale this for difficult problems but for the OP's problem, a solution is pretty short:

1. Take: A = "A is a knight", B = "B is a knight", Z = "A is a knave" and Y = "B is a knave"
2. By definition: A+Z = B+Y = 1
3. Inclusive p or q is "p + q - pq = 1"
4. The claims give us the equations: Z + AB + YZ - ABYZ = 1 and Y + AY + BZ - ABYZ = 1
5. ABYZ = 0 so Z + AB + YZ = Z(1 + Y) + AB = 1 and Y + AY + BZ = Y(1 + A) + BZ = 1
6. Using (2) (1+Y) = B and (1+A)=Z, substituting in (5) we end up with: B(Z+A)=1 and Z(Y+B)=1
7. Then B=1 and Z=1, that is, A is a knave and B is a knight.