Proof
Immerman 1999 provides a detailed proof of the theorem. Essentially, we use second-order existential quantifiers to arbitrarily choose a computation tableau. For every timestep, we arbitrarily choose the finite state control's state, the contents of every tape cell, and which nondeterministic choice we must make. Verifying that each timestep follows from each previous timestep can then be done with a first-order formula.
A key idea from the proof is that we can encode a linear order of length nk as a 2k-ary relation R on a universe A of size n. To achieve this, we choose a linear ordering L of A and then define R to be the lexicographical ordering of k-tuples from A with respect to L.
Read more about this topic: Fagin's Theorem
Famous quotes containing the word proof:
“If any doubt has arisen as to me, my country [Virginia] will have my political creed in the form of a “Declaration &c.” which I was lately directed to draw. This will give decisive proof that my own sentiment concurred with the vote they instructed us to give.”
—Thomas Jefferson (1743–1826)
“Talk shows are proof that conversation is dead.”
—Mason Cooley (b. 1927)
“When children feel good about themselves, it’s like a snowball rolling downhill. They are continually able to recognize and integrate new proof of their value as they grow and mature.”
—Stephanie Martson (20th century)