 In his short 1936 note Post considers machines that either mark or unmark a square which means we have only two symbols \(S_0\) and \(S_1\) but he did not prove that this formulation captures exactly the Turing computable functions. It was Shannon who proved that for any Turing machine T with n symbols there is a Turing machine with two symbols that simulates T (Shannon 1956). He also showed that for any Turing machine with m states, there is a Turing machine with only two states that simulates it.