I’ve formalized this problem in Coq with mathcomp. Yeah, idk why I decided to do this.
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition hats_assignment : Type := nat -> bool.
Definition policy_of_one_person (n : nat) : Type :=
{policy : hats_assignment -> bool &
forall ha : hats_assignment,
let ha' := fun m => if m == n is true then ~~ (ha m) else ha m
in policy ha == policy ha'}.
Definition strategy : Type :=
forall n : nat, policy_of_one_person n.
Lemma ex_good_strategies :
exists s : strategy, forall ha : hats_assignment, exists N : nat, forall n : nat, n >= N ->
(projT1 (s n)) ha == ha n.
Proof.
Admitted.
If you want to solve it, you need to replace Admitted. with an actual proof.
For clarification, the people can all see the color of other people’s hats, right? If so, then:
The people agree in advance (using the axiom of choice!) on a set of representatives for all equivalence classes in 2N/∼, where two bit sequences are equivalent under ∼ iff they differ in only finitely many positions.
When they are guessing, they all know the equivalence class they are in and they guess the color for their hat that is implied by the agreed upon representative of that equivalence class. By construction, only finitely many of them can guess incorrectly.
We can assume that they can each magically agree on the same strategy, and that as they are countably infinite they can find a common ordering of them.
A countably infinite number of people are each assigned a hat that is either red or blue.
Without communication, they must each guess the color of their hat. The cannot know of each others guesses.
Show that there exists a strategy by which only a finite number of people will guess incorrectly.
I’ve formalized this problem in Coq with mathcomp. Yeah, idk why I decided to do this.
If you want to solve it, you need to replace
Admitted.with an actual proof.This is great.
For clarification, the people can all see the color of other people’s hats, right? If so, then:
The people agree in advance (using the axiom of choice!) on a set of representatives for all equivalence classes in 2N/∼, where two bit sequences are equivalent under ∼ iff they differ in only finitely many positions.
When they are guessing, they all know the equivalence class they are in and they guess the color for their hat that is implied by the agreed upon representative of that equivalence class. By construction, only finitely many of them can guess incorrectly.
Yes they can see each others hats.
Do people have common knowledge of an ordering of all of them?
We can assume that they can each magically agree on the same strategy, and that as they are countably infinite they can find a common ordering of them.