the Immerman-Szelepcsenyi theorem
/ IM-er-man SEL-eh-PCHAYN-yee /
Here is the second great surprise that makes space behave unlike time. Nondeterministic machines are good at confirming that something exists (a path, a satisfying assignment) by guessing it, but seem hopeless at confirming that something does NOT exist, since there is no single object to guess. For time we have no idea whether NP equals co-NP (most believe not). Yet for nondeterministic space, the impossible-seeming becomes possible: it is closed under complement. The Immerman-Szelepcsenyi theorem (Neil Immerman and Robert Szelepcsenyi, independently, 1987) proves it.
Formally, for any space bound f(n) at least log n, NSPACE(f(n)) equals co-NSPACE(f(n)). The headline case is NL equals co-NL: a problem solvable in nondeterministic log space has its complement also solvable in nondeterministic log space. Take directed reachability. Confirming that t IS reachable from s is easy for an NL machine (guess the path). The clever part is confirming that t is NOT reachable, with only log space. The proof uses inductive counting: the machine nondeterministically computes the exact NUMBER of vertices reachable from s within k steps, building it up from k to k+1, and once it knows that count it can verify, vertex by vertex, that t is not among the reachable ones, all while storing only a few counters.
This is genuinely shocking because the analogous statement for time (NP equals co-NP) is widely believed false and is wide open. The reason space can do it again comes down to reuse: counting and re-verifying can overwrite the same cells, whereas an NP verifier cannot re-derive the absence of a witness within its time budget. The theorem also cleaned up the landscape of context-sensitive languages (NSPACE(n)), settling a long-standing question about their closure under complement. Caveat: the counting trick needs the exact reachable-set size, which the machine itself guesses and then verifies nondeterministically; it is subtle, not a one-line argument.
Non-reachability is in NL thanks to this theorem. To certify that t is NOT reachable from s, the machine first nondeterministically computes c, the exact number of vertices reachable from s. Then, for each vertex other than t, it guesses-and-verifies a path proving it reachable, and checks that exactly c such vertices are confirmed without ever confirming t. Only counters of size O(log n) are stored.
Inductive counting lets an NL machine certify NON-reachability, proving NL = co-NL.
The time analogue, NP = co-NP, is OPEN and widely believed false. Space pulls off NL = co-NL through reuse (re-deriving counts in the same cells), which a time-bounded verifier cannot imitate.