Cellular automaton axioms

The first 4 axioms are general to one-dimensional cellular automata. The next 8 are specific to rule 110. The final 3 work whenever patterns are embedded in a background of white cells. The universality of rule 110 presumably implies that the axiom system given is universal. (A complete proof would require handling various issues about boundary conditions.)

If the last 2 axioms are dropped any statement can readily be proved true or false essentially just by running rule 110 for a finite number of steps equal to the number of nested ↓ plus 〈 … 〉 in the statement. In practice, a large number of steps can however be required. As an example the statement

○ ■  (∃_a (∃_b ○ a ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (□ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (□ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (□ ⋄ (□ ⋄ (□ ⋄ (■ ⋄ (□ ⋄ (□ ⋄ (■ ⋄ (■ ⋄ (□ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (■ ⋄ (□ ⋄ (□ ⋄ (□ ⋄ (■ ⋄ (□ ⋄ b)))))))))))))))))))))))))))))))))))))

asserts that a particular localized structure occurs in the evolution of rule 110 from a single black cell. But page 38 shows that this happens for the first time after 2867 steps. (A proof of this without lemmas would probably have to be of length at least 32,910,300.)

The axioms as they are stated apply to any rule 110 evolution, regardless of initial conditions. One can establish that the statement at the bottom on the right cannot be proved either true or false from the axioms by showing that it is true for some initial conditions and false for others. Note from page 279 that the sequence cannot occur in rule 110 evolution except as an initial condition. So this means that the statement is false if the initial condition is and true if the initial condition is .