I am trying to understand the mathematical content of the free will theorem. See this link or just the wikipedia pages and the references therein.
I think the main point of the theorem is the following.
Let $3D$ be the set of triples of orthogonal lines ($1$-dimensional vector subspaces) in $\mathbb{R}^3$, let $D$ be the set of lines.
An even (non-constant) triple is an element of $ET := \{(0,1,1),(1,0,1),(1,1,0)\}$.
Theorem: There is no couple $(f,g)$ such that:
- $f$ is a map from $3D$ to $ET$;
- $g$ is a map from $D$ to $\{0,1\}$;
- for all couples $(t,d) \in 3D \times D$, for all $i \in \{1,2,3\}$, if $t(i) = d$ then $g(d) = f(t)(i)$.
Proof: It is easily seen that if such a couple $(f,g)$ exists, then $g$ is a map sending each line to $0$ or $1$ such that for every triple $(d_1,d_2,d_3)$ of orthogonal lines, there is exactly one that is sent to $0$. This is called a $101$-function and a clear proof that a $101$ function does not exist can be found at page $227$ of the linked paper.
Remark: It is enough to restrict attention to a finite subset of $D$ and the corresponding subset of $3D$, and the theorem still works, making everything finite.
However, what I don't understand is the rest of the proof. The authors talk about functions of of "information", (sometimes, information is "free", and sometimes it is not). Moreover, the sentences of the form "if $\alpha$ depends on $x$, then one can introduce $x$ as a new argument and, by changing the function, one can assume that this doesn't depend on $x$ anymore" are gibberish to me, despite all the respect I feel for Conway.
Can you help me understand the rest of the proof? Can you provide me with a reference containing a formal version of the proof?
