There are several ways to describe the semantics of nondeterministic Turing machines. Perhaps the most colorful is the "guess and verify" semantics. We enhance a vanilla Turing machines with a guess tape, whose exact semantics will be explained below. Our Turing machine communicates its computation with the user by means of the state at which it halts. Some states are marked ACCEPT, the rest are marked REJECT. The semantics of the machine are as follows:

> A nondeterministic machine accepts an input $x$ if there exists a string $y$ such that if we run the machine with $x$ on the input tape and $y$ on the guess tape, then it accepts (i.e., halts at a state marked ACCEPT).
>
> Conversely, the machine rejects an input $x$ if whenever we run the machine with $x$ on the input tape and *arbitrary* contents on the guess tape, it always rejects (i.e., halts at a state marked REJECT), whatever we wrote on the guess tape.
>
> A nondeterministic machine accepts a language $L$ if it accepts all $x \in L$ and rejects all $x \notin L$.
>
> A nondeterministic machine *runs in polynomial time* (*polytime* for short) if there is a polynomial $p(n)$ such that whenever we run the machine with $x$ on the input tape and arbitrary contents on the guess tapes, it always halts within $p(|x|)$ steps.

(We are slightly cheating here: the definitions of acceptance and rejection are complementary only if the machine is promised to always halt, which is indeed the case for machines running in polynomial time.)

---

When describing the operation of a nondeterministic machine, we will often use the keywords "guess" and "verify". They have the following meaning:

1. **Guess $w$**: Copy a string $w$ (delimited in some fixed way) from the guess tape to the work tape.
1. **Verify property $A$**: Check whether property $A$ holds. If so, continue with the execution of the algorithm. Otherwise, halt at once at a state marked REJECT.

Another important convention is:

* If the algorithm runs its course without rejecting, then the machine halts at a state marked ACCEPT.

Here is an example, a machine for SAT:

> Input: A formula $\varphi$ in conjunctive normal form.
>
> Operation: Guess an assignment $a$, and verify that it is a satisfying assignment.

A more exact description of the machine would be:

> 1. Copy an assignment $a$ from the guess tape to the work tape.
>
> 1. Check whether $a$ satisfies $\varphi$.
>
> 1. If $a$ doesn't satisfy $\varphi$, halt at a state marked REJECT.
>
> 1. Otherwise, halt at a state marked ACCEPT.

---

Let us now consider the proof that NP is closed under intersection. Let $M_1,M_2$ be polytime nondeterministic Turing machines accepting languages $L_1,L_2$ (respectively). The following polytime nondeterministic Turing machine $M$ accepts $L_1 \cap L_2$:

> 1. Verify that $M_1$ accepts the input.
> 1. Verify that $M_2$ accepts the input.

In more detail:

> 1. Decode the contents of the guess tape into two guess words.
> 1. Run $M_1$ on the inputs and the first guess word. If it halts at a state marked REJECT, enter a state marked REJECT and halt.
> 1. Run $M_2$ on the inputs and the second guess word. If it halts at a state marked REJECT, enter a state marked REJECT and halt.
> 1. Enter a state marked ACCEPT and halt.

Why does this work? Let $L$ be the language accepted by this machine. We have to show that $L = L_1 \cap L_2$.

1. $L_1 \cap L_2 \subseteq L$: Suppose that $x \in L_1 \cap L_2$. Since $x \in L_1$, there exists a string $y_1$ such that $M_1$ accepts when run on $x$ with $y_1$ on the guess tape. Similarly, since $x \in L_2$, there exists a string $y_2$ such that $M_2$ accepts when run on $x$ with $y_2$ on the guess tape. If we run $M$ on $x$ with $(y_1,y_2)$ on the guess tape, then it will accept, and so $x \in L$.

1. $L \subseteq L_1 \cap L_2$: Suppose that $x \in L$. Thus there is a string $y = (y_1,y_2)$ such that when $M$ is run on the input $x$ and $y$ on the guess tape, it accepts. The machine $M$ verifies that $M_1$ accepts when run on the input $x$ and $y_1$ on the guess tape, and that $M_2$ accepts when run on the input $x$ and $y_2$ on the guess tape. Therefore $x \in L_1$ and $x \in L_2$, and so $x \in L_1 \cap L_2$.

---

Now let us try to prove that NP is closed under complementation. Let $M$ be a polytime nondeterministic Turing machine accepting a language $L$. We construct the following Turing machine $M'$:

> Run $M$. If $M$ accepts, reject. Otherwise, accept.

Let us see what are the semantics of this machine. The machine $M'$ accepts an input $x$ if there exist a string $y$ such that when running $M$ on $x$ with $y$ on the guess tape, it rejects. Conversely, the machine $M'$ rejects an input $x$ if $M$ accepts $x$ regardless of the contents of the guess tape.

This is not quite what we want, and to demonstrate it, let us consider the machine $M$ accepting SAT described above. Recall that the machine interprets its input as a formula $\varphi$, and the contents of the guess tape as an assignment $a$. The machine $M$ accepts iff $a$ satisfies $\varphi$. The corresponding machine $M^c$ has the following semantics:

1. The machine $M^c$ accepts a formula $\varphi$ if some assignment $a$ doesn't satisfy $\varphi$.

1. The machine $M^c$ rejects a formula $\varphi$ if all assignments $a$ satisfy $\varphi$.

In other words, the machine $M^c$ accepts the language of all formulas which are not tautologies. This is not what we were aiming for: we wanted $M^c$ to accepts the language of all unsatisfiable formulas. As an example, $M^c$ accepts the formula $x_1 \lor x_2$ even though it is satisfiable, because it's not a tautology (if $x_1$ and $x_2$ are both false then $x_1 \lor x_2$ is also false).