It occurs to me that the sort of reasoning common in many logic puzzles (e.g. https://en.wikipedia.org/wiki/Hat_puzzle or https://xkcd.com/blue_eyes.html), the persons involved all trust one another to behave perfectly rationally, and will make all possible sound deductions. If we assume that they all believe in axioms at least as strong as Peano Arithmetic (which is quite a reasonable assumption, I think), then it seems that this scenario is actually rather self-defeating via Godelian results, in particular Lob's Theorem. In other words, a person can reason in the following degenerate manner in a hat puzzle:
Both I (A) and the person next to me (B) have common knowledge that we are perfectly rational and correct reasoners. B accepts me as a rational and correct, so he will accept the statement, "If A can prove that 1+1=3, then A will conclude this statement, and I trust A as rational and correct, so 1+1=3." I trust B to reason rationally and correctly, so he will conclude this statement, and because I accept any statement that B accepts, I accept that if I can prove 1+1=3, then 1+1=3. By Lob's Theorem, 1+1=3.
The reasoning I'm making here is quite informal, so I'm not sure if I've made a subtle mistake, but I don't see any easy way around Godelian issues here. In order for the solutions to work, the people involved need to assume the others can perform reasoning about the natural numbers including induction, need to believe that others will prove anything that is provable, and need to believe that others will always come to sound conclusions. Is there any way we can recover the solutions to this sort of puzzle without allowing degenerate "solutions" like the above? In other words, can the assumptions about common knowledge and rationality here be formulated in a way that is provably consistent, while still allowing the commonly accepted solutions to these puzzles?