Any truth assignment that satisfies the clauses we've talked about so
far specifies how the tableau should be filled out and
moreover, the tableau will always start on the initial configuration and
end up in an accepting one.
What is not guaranteed yet
is that the transitions between the configurations are valid.
To see how we can add constraints that will give us this guarantee,
we'll use this example.
Suppose that the transition function tells us that if the machine is in state
q3, and it reads a 1 then it can do one of two things.
It can move to state q0, leaving the 1 alone and move the head to the right,
or it can move to state q4, write a 0 and move the head to the left.
To translate this rule into clauses for
our formula, it's useful to make a few definitions.
First, we need to enumerate the tape alphabet so
that we can refer to the symbols by number.
Let's say that the blank is symbol 0, 0 is symbol 1 and 1 is symbol 2.
Next, we define the tuple k, l, k prime, l prime,
delta to be valid if the triple of the state qk prime,
sl prime and delta is in the set delta of qk, sl.
That is to say, this has to be one of the valid transitions,
given that we are in state qk and that we read the symbol sl.
For example, the tuple 3, 2, 0, 2, R is valid.
The first two numbers here indicate which transition rule applies.
And note here that I'm using the enumeration of the alphabet
to translate the symbols here.
3 means state three and 2 means the symbol one.
The last three numbers indicate the transition being made.
In this case it is in the set defined by delta.
We're moving to state q0, we're writing symbol 2, which is a 1.
And we're moving to the right.
On the hand, this transition is endowed, the machine can't switch to state four,
write a one, and move the head to the right.
That's not one of the valid transitions,
given that the machine is in state three, and that it just read a blank.
Now there are multiple ways to create the causes needed to ensure that
only valid transitions are followed.
Many proofs of Cook's theorem start by writing out Boolean expressions,
that directly express the requirement that one of the valid
transitions be followed.
The difficulty with this approach,
is that the intuitive expression isn't in conjunctive normal form.
And some Boolean algebra is needed to convert it.
That is to say, we don't immediately get an intuitive set of short clauses
to add to our formula.
On the other hand, if we rule out invalid transitions instead, then we
do get a set of short intuitive clauses that we can just add to the formula.
To illustrate, in order to make sure that this invalid transition is never
followed, for every step i and position j, we add a clause that looks like this.
It starts with three literals that ensure the transition rules for
being in state q3 and reading a blank symbol actually do apply.
If the head isn't in the position we're talking about, the state isn't q3, or
the symbol being read isn't the blank symbol,
then the clause is immediately satisfied.
The clause can also be satisfied if the machine behaves
in any way that's different from what this particular
invalid transition would cause to happen.
The head could move differently, the state could change differently, or
a different symbol could be written.
Another way to parse this clause is as saying if the Q3 blank symbol transition
rule applies, then this invalid transition can't have been followed.
Logically remember that A implies not B is equivalent to not A or not B.
That's the logic we're using here.
A being, does the transition rule apply, and
B being, was the invalid transition followed.