Let me first pose the problem:
The king of some faraway land is bored, so he decides to setup a little game for his own amusement. These are the rules of the game:
7 prisoners will be seated at a round table. Each prisoner will have a hat placed on their head. Each hat is one of seven possible colors. The prisoners can see everyone else's hat, but they cannot see their own. The prisoners will then write on a piece of paper what they think their hat color is, and hand the paper to the king.
If any of the prisoners guesses their hat color correctly, they will all go free. Otherwise, they are all executed on the spot.If the prisoners use the naive strategy of guessing randomly, then they have a survival chance of 66%. Can you think of a strategy such that the prisoners have a 100% chance of survival?
When given this problem, my brain subconsciously pointed towards modular arithmetic and I gave a satisfactory answer that solved the problem. My answer matched the answers given in this Math SE answer: Rainbow Hats Puzzle
A person I was explaining this problem to said that the answer worked in retrospect, but it required a logical leap to arrive at the answer. Introspection revealed that I too took a subconscious shortcut towards modular arithmetic without natural deduction.
My question is this: Is there a way to solve this systematically without a logic leap and with natural deduction or inferences. Understanding the modular arithmetic answer is easy in retrospect, but explaining how one might arrive at the solution is much harder.
Best Answer
I didn't know the problem in this particular form before and just solved it on my own using modular arithmetic. I will tell you my thinking process, hoping it suffices to answer your question.
A prisoner sees six hats and has to make a guess for the colour of their own hat. Of the seven colours possible, they will guess correctly exactly once. That means, a prisoner will call the correct colour for exactly one seventh of the $7^7$, that is $7^6$, possible distributions of hats to prisoners. In total, we get $7^7$ correct guesses from all seven prisoners for $7^7$ cases. That means we cannot waste even a single correct guess. We have to make sure that in each case exactly one of the prisoners guesses correctly.
Let $C$ be the set of colours and $P = \{1,\dotsc,7\}$ the set of prisoners. Suppose we already know a solution to the puzzle. Since for each hat distribution $c \in C^7$ there is a correct call from exactly one prisoner, we can form the function $f \colon C^7 \to P$, where $f(c) = p$ if $p$ is the one to guess correctly on hat distribution $c$. This function has an interesting property: Let $p \in P$ be a prisoner and fix colours $c_q \in C$ for all prisoners $q \neq p$. Then there is exactly one colour $c_p$ such that $f((c_q)_{q \in P}) = p$. This is just the fact that $p$ guesses exactly one colour when they see hats $(c_q)_{q \neq p}$.
This correspondence between solutions of the puzzle and functions goes both ways. Given a function $f$ as above, the prisoners can use the following strategy: If $p \in P$ sees hats $(c_q)_{q \neq p}$, have $p$ guess the unique colour $c_p$ such that $f((c_q)_{q \in P}) = p$. Then on hat distribution $c$, prisoner $f(c)$ guesses correctly.
If we can construct an $f$ as above, we are done. The special property it has to fulfill is a bit weird, though. It becomes more managable if we replace it by something stronger. Instead of only expecting a unique $c_p$ such that $f((c_q)_{q \in P}) = p$, we can demand a unique $c_p$ such that $f((c_q)_{q \in P}) = p'$ for all $p' \in P$, not just $p' = p$. Another way to phrase this: After fixing colours $c_q$ for $q \neq p$, the map $C \to P$ sending the remaining colour $c_p$ to $f((c_q)_{q \in P})$ is bijective.
We are now looking for a function $C^7 \to P$ that is bijective in each argument when leaving the other six fixed. You wanted to use modular arithmetic, so identify both $C$ and $P$ with $\mathbb{Z} / (7)$. Then we need a map $(\mathbb{Z} / (7))^7 \to \mathbb{Z} / (7)$ bijective in each argument. Just adding up all the seven arguments should work.
Note: I did not formalize the correspondence between solutions and functions $f$ before writing this down. I thought about what was needed to reconstruct a valid strategy from $f$. At first I noted that $f$ being in bijective in each argument works. I figured out the exact condition on $f$ after I had the solution already.