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

[ 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).

• What is the point of this formalization with "natural deduction"? – Zubin Mukerjee Dec 7 '19 at 15:53
• I'm interested in finding a mechanical way to solve that kind of problem. When intuition is dumb, it can be usefull to rely on that kind of method. – Saint James Dec 7 '19 at 15:58
• @ZubinMukerjee In case you are not familiar with this style of problem, the rule is that knights make only true statements and knaves make only false statements. – Matthew Daly Dec 7 '19 at 16:36
• @MatthewDaly Ah ok, that makes a lot more sense ... excuse my ignorance. You are right, I didn't know the knaves were liars – Zubin Mukerjee Dec 7 '19 at 16:59
• @ZubinMukerjee I can't imagine how frustrating it would be to try to follow this conversation without knowing that. I'll go edit this question as a warning to others. ^_^ – Matthew Daly Dec 7 '19 at 17:09

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}$$

• That must be the quickest way indeed! – Saint James Dec 7 '19 at 17:06
• @EleonoreSaintJames Well, remember it all depends on what inference/equivalence rules you have. Thus, theoretically, the quickest way is always $1$ step ... if you have some weird system that happened to have the inference from the premise to the conclusion as one of its inference rules! But, in practice, we use of course 'basic' inference principles; that's of course the whole point of a proof; to break down the reasoning to elementary inferences. So, as long as you stick to 'reasonable' inferences, I do believe my derivation is about as short as possible, yes. – Bram28 Dec 7 '19 at 17:10
• @EleonoreSaintJames Also, note that the length of the proof also depends on how the given information is being represented. Matt Daly and I both used biconditionals, whereas you used a conjunction to represent Bill's statement. And while I used $\neg J \leftrightarrow \neg B$ to represent John's statement, Matt Daly used $J \leftrightarrow B$ which, for the Fitch-style system he is using, makes the proof 3 steps shorter than would he have used $\neg J \leftrightarrow \neg B$. – Bram28 Dec 7 '19 at 17:17
• If you had substitutivity of equivalence, you'd be able to get to $B\equiv\neg J$ right after the givens and solve in four steps. Smullyan might give the following proof in text form "John and Bill disagree, so they cannot be the same type. But that's exactly what Bill said -- he must be a knight because his statement is true. Therefore, John is a knave." – Matthew Daly Dec 7 '19 at 20:46
• @MatthewDaly Oooh, nice! Let me add your suggestion to my post, thanks! – Bram28 Dec 7 '19 at 20:48

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.