I was looking at a 'knight and knave' problem from one of Smullyan's puzzle books and found this:

There are 3 persons: A,B,C

- At least one is a Knight.
- At least one is a Knave.
- One of them has a prize.
Each has a statement to say:

- A says: B doesn't have the prize
- B says: I don't have the prize
- C says: I have the prize
Who has the prize?

Would it be possible to solve this with coq?

What could be the goal? Goal is an assignment from {Knight, Knave} to variables A,B,C.

How can that even be stated?

(And how can we reduce this to SAT problem? Is that possible?)

I started like:

```
Inductive type : Set := K | V.
Inductive person : type -> Type :=
| Person: forall t:type, person t.
Axiom hasP: forall {t:type}, person t -> Prop.
Definition isK {t:type} (p:person t): Prop :=
match t with
| K => true
| _ => false
end = true.
Goal
exists (t1 t2 t3:type),
forall (a:person t1) (b:person t2) (c:person t3),
(t1=K \/ t2=K \/ t3=K) /\
(t1=V \/ t2=V \/ t3=V) /\
(hasP a \/ hasP b \/ hasP c) /\
(isK a -> ~hasP b) /\
(isK b -> ~hasP b) /\
(isK c -> hasP c).
```

`Inductive person := a | b | c.`

and `assignment : person -> type`

might be effective

Also: your formalization only requires knights to be honest. Are knaves not expected to lie?

Using person := a | b | c also lets you avoid forall. And since type is isomorphic to boolean, then that's basically already a SAT problem!

Paolo Giarrusso said:

`Inductive person := a | b | c.`

and`assignment : person -> type`

might be effective

Sorry for a reply to an old post, but in this case, does `assignment`

would have to be an axiom, right? Or should it be made a `Definition`

giving a `Prop`

?

I think neither? `Section with_assignment. Context (assignment : person -> type).`

Sorry, misread. Your overall goal seems `exists assignment ...`

Yeah, like `exists t1 t2: type, assignment a = t1 /\ assignment b = t2 /\ ...`

kind of thing is what I was looking it.

Am trying to read this now: https://www.cs.ru.nl/bachelors-theses/2022/Kimberley_Frings___1027103___Formalizing_and_proving_knights_and_knaves_puzzles_in_three_valued_logic_in_Coq.pdf

I gave your puzzle a try and found a set-up like this fairly simple to use:

```
Inductive Person :=
A | B | C.
Section KnightAndKnave.
Variable knight : Person.
Variable knave : Person.
Variable prize_holder : Person.
Definition statement (p : Person) : Prop :=
match p with
| A => prize_holder <> B
| B => prize_holder <> B
| C => prize_holder = C
end.
Hypothesis knight_tells_truth :
statement knight.
Hypothesis knave_tells_lie :
~ statement knave.
(* replace X with who you think has prize *)
Theorem X_has_prize : prize_holder = X.
Proof.
Admitted.
End KnightAndKnave.
```

A tiny issue I have with the `assignment : person -> type`

model of the problem is that it forbids by fiat a person from being both knight and knave (or neither, I suppose). Of course, the fact that one cannot be both is an easy logical consequence, but then you should prove it if necessary instead of pushing it into your axioms.

is there a reason there can't there be several knights or several knaves?

Hm, the problem statement is incomplete — I'm used to "everybody is either a knight or a knave, knights are always truthful, knaves always lie" always being part of these problems.

If not, you should have predicates `knight, knave : person -> bool`

(using `Prop`

might force you to use classical logic unnecessarily).

bonus: prove directly from the characteristics of a knight and a knave that a person can't be *both*. But probably one wants to keep the possibility to be *neither*.

I would argue that making (the property of being) `knight`

and `knave`

decidable is against the spirit of the puzzle setup, though

and in some sense it gives information about the nature of the puzzle if one finds oneself in the situation of needing to use classical logic

Last updated: Jun 18 2024 at 09:02 UTC