Knights and Knaves problem There are 3 individuals, A, B, and C, each of which is either a Knight or a Knave. Knights always tell the truth; Knaves always lie.  These are the statements each makes:


*

*A says exactly one of the three is a knave

*B says exactly two of the three are knaves

*C is silent


I need to solve this problem with a proof. I was able to formalize the statements but they are so extremely long that I am not sure how to go about solving this via a proof. It would be helpful if I knew of a simpler way to write statement A and B rather than saying (A&B&~C) OR (A&~B&C) OR (~A&B&C) for A's statement and (A&~B&~C) OR (~A&B&~C) OR (~A&~B&C) for B.
 A: This answers the original question:
A says exactly one of the three is a knave
B says exactly two of the three are knaves
C says they are all knaves
If I understand correctly, I suppose each person is either a knight or a knave, that is they always tell the truth or always lie, depending upon which type of person they are.
If that is the case, C must be lying, for if all 3 were knaves, C would be telling the truth, which is impossible. C is a knave.
B may be telling the truth, because C is a knave and if B is telling the truth, then A is lying. (possible scenario A- Knave, B-Knight, C-Knave).
Suppose instead that A is a knight, then there are 2 knights. We have already established that C is a knave, so B must be a knight. But B says there are 2 knaves. Contradiction.
Thus B must be the only knight.

An alternate approach. The 3 statements are mutually exclusive. Exactly one of them is telling the truth or they are all lying (in other words, at most one of these statements is true). If they are all lying, then C is right, but then C's not lying. Thus it must be that exactly one of them is telling the truth.
Thus there is only one knight. Thus there are 2 knaves. Thus B's statement is true, making him the knight.

with the current version ( C is instead silent),
A and B's statements are mutually exclusive, so they cannot both be knights. Thus the scenario must be one of the following (A means A is a knight, ~A means A is a knave, and similar for others):

*

*(A,~B, either), but if A is telling the truth, then C must be a knave: (A,~B,~C)

2.(~A,B, either), but if B is telling the truth, then C must be a knight: (~A,B,C)
3.(~A,~B, either). If A and B are both lying, then they must all 3 be knaves (~A,~B,~C).
This version has 3 possible solutions. They are all knaves, A is the only knave; or A is the only knight.
A: You could use your own defined connective like $ONE(A,B,C)$ that returns True iff exactly one of the variables returns True. Similarly you can define $TWO(A,B,C)$, $ALL(A,B,C,D)$, $NONE(A,B,C,D,E)$, etc. You get the point.
Then you can define some obvious inferences using these. For example:
$ALL(P_1, ..., P_n)$
$\therefore P_i$
Or:
$TWO(P_1, .., P_n)$
$P_i$
$\therefore ONE(P_1,...P_{i-1}, P_{i+1},...,P_n)$
Or:
$NONE(P_1, ..., P_n)$
$P_{n+1})$
$\therefore ONE(P_1,...,P_n,P_{n+1})$
Etc. Again, you get the point.
And with that, you can still formalize a proof as usual. It won't just have the standard set of connectives, but you do have the same rigor and organization as a standard logic proof, and that's what matters.
