Immerman–Szelepcsényi: NL = coNL

The theorem (Immerman 1988, Szelepcsényi 1988): nondeterministic logarithmic space is closed under complement. In this library the class NL is defined by the Krom fragment of existential second-order logic (DescriptiveComplexity.NL), and the theorem is assembled from three pieces:

• DescriptiveComplexity.TCDefinable.compl – FO(TC) is closed under complement, the content of the theorem, proved by the inductive-counting machine of DescriptiveComplexity.InductiveCounting run inside a single transitive closure (DescriptiveComplexity.TransitiveClosureCompl);
• the two translations between the Krom fragment and FO(TC), which say that SO-Krom definability is FO(TC) definability of the complement (DescriptiveComplexity.sigmaSOKromDefinable_iff_tcDefinable_compl);
• the definitional duality between a class and its complement class.

Three consequences are recorded here beyond NL = coNL itself: NL is FO(TC) (DescriptiveComplexity.tcDefinable_iff_mem_NL), which the two translations alone could not say; the Krom fragment is closed under complement, which no inspection of clauses could give; and REACH ∈ NL (DescriptiveComplexity.reach_mem_NL), the membership a clausal fragment cannot state directly because it defines non-reachability head-on.

FO(TC) is closed under complement

theorem DescriptiveComplexity.TCDefinable.compl {L : FirstOrder.Language} {P : DecisionProblem L} (h : TCDefinable P) : TCDefinable Pᶜ

Immerman–Szelepcsényi: on finite ordered structures, the complement of an FO(TC) definable problem is FO(TC) definable.

The specification of the complement is the inductive-counting machine: its modes are the control states (a phase, one flag and the mode of each of eight registers) and its tuples hold the eight registers side by side, so that counting the nodes of every layer of the given walk – and certifying, at the last layer, that no accepting node was ever counted in – is itself one walk.

theorem DescriptiveComplexity.tcDefinable_compl_iff {L : FirstOrder.Language} (P : DecisionProblem L) : TCDefinable Pᶜ ↔ TCDefinable P

Complementation is a bijection of the FO(TC) definable problems.

NL = coNL

theorem DescriptiveComplexity.tcDefinable_iff_mem_NL {L : FirstOrder.Language} (P : DecisionProblem L) : TCDefinable P ↔ NL.Mem P

NL is FO(TC): a problem is in NL exactly when it is FO(TC) definable. The two translations against the Krom fragment give this only up to a complement; Immerman–Szelepcsényi removes it.

theorem DescriptiveComplexity.sigmaSOKromDefinable_compl_iff {L : FirstOrder.Language} (P : DecisionProblem L) : SigmaSOKromDefinable Pᶜ ↔ SigmaSOKromDefinable P

The Krom fragment is closed under complement: a statement about a clausal fragment that no inspection of its clauses provides – it is Immerman–Szelepcsényi, read through the translations to FO(TC).

theorem DescriptiveComplexity.NL_eq_coNL : NL = coNL

NL = coNL (Immerman 1988, Szelepcsényi 1988): nondeterministic logarithmic space is closed under complement.

theorem DescriptiveComplexity.mem_NL_compl_iff {L : FirstOrder.Language} (P : DecisionProblem L) : NL.Mem Pᶜ ↔ NL.Mem P

Membership in NL is closed under complement.

REACH is in NL

theorem DescriptiveComplexity.reach_mem_NL : NL.Mem REACH

REACH ∈ NL: directed reachability belongs to nondeterministic logarithmic space. The Krom fragment defines non-reachability head-on – a clausal fragment states closure and rejection – so this membership is exactly what Immerman–Szelepcsényi adds.