UNREACHd, and L = coL

Deterministic logarithmic space is closed under complement (DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE), and UNREACHd – non-reachability along forced arcs – is LOGSPACE-complete (DescriptiveComplexity.UNREACHd_LOGSPACE_complete).

Unlike NL = coNL this needs no inductive counting, and unlike the clausal fragments FO(DTC) has no built-in asymmetry between a problem and its complement: everything reduces to one membership statement, DescriptiveComplexity.unreachd_dtcDefinable. Given it, the complement of any FO(DTC) definable problem is FO(DTC) definable, because a reduction complements along with the problem (DescriptiveComplexity.OrderedFOReduction.compl) and REACHd is LOGSPACE-hard.

Complementing a deterministic walk

REACHdᶜ says that no marked source has a marked target ahead of it. Three things make that a deterministic walk:

• The walk is functional, so from a given vertex there is only one thing to do: follow the forced arc (DescriptiveComplexity.detNext, the successor map, a dead end being its own successor). Reachability along forced arcs is exactly iteration of that map (DescriptiveComplexity.reflTransGen_detEdge_iff_iterate).
• A step budget replaces cycle detection. A walk that has not arrived after |A| - 1 steps never will: taking a minimal number of steps to a vertex makes the visited vertices distinct, so it is bounded by the size of the universe (DescriptiveComplexity.exists_iterate_lt_card). The budget is carried as a third coordinate holding a vertex, counted through DescriptiveComplexity.orank – the universe has exactly as many elements as the walk may take steps.
• The sources are scanned in order. Acceptance quantifies the start node existentially, while the complement must quantify sources universally, so the walk loops over the candidates itself, in the order of the structure, and accepts only after exhausting them.

A node is therefore a mode – scanning or done – with a triple (s, x, c): the source candidate, the current position, the budget. The walk gets stuck exactly when it finds a marked target ahead of a marked source, so it reaches its accepting node exactly when there is nothing to find.

The forced-arc successor map

theorem DescriptiveComplexity.detEdge_unique {A : Type} [FirstOrder.Language.stGraph.Structure A] {x y z : A} (hy : DetEdge x y) (hz : DetEdge x z) : y = z

The forced arcs are functional: that is the whole point of DescriptiveComplexity.DetEdge.

def DescriptiveComplexity.Stuck {A : Type} [FirstOrder.Language.stGraph.Structure A] (x : A) : Prop

A vertex is stuck when no arc out of it is forced: either it has no outgoing arc at all, or it has several.

Equations

• DescriptiveComplexity.Stuck x = ¬∃ (y : A), DescriptiveComplexity.DetEdge x y

noncomputable def DescriptiveComplexity.detNext {A : Type} [FirstOrder.Language.stGraph.Structure A] (x : A) : A

The successor map of the deterministic walk: the endpoint of the forced arc out of x, and x itself where the walk is stuck – the walk of the forced arcs read as an iterated function, DescriptiveComplexity.stepNext. Making it total is what lets reachability be read as iteration.

Equations

• DescriptiveComplexity.detNext x = DescriptiveComplexity.stepNext DescriptiveComplexity.DetEdge x

theorem DescriptiveComplexity.detEdge_detNext {A : Type} [FirstOrder.Language.stGraph.Structure A] {x : A} (h : ¬Stuck x) : DetEdge x (detNext x)

theorem DescriptiveComplexity.detNext_eq_self {A : Type} [FirstOrder.Language.stGraph.Structure A] {x : A} (h : Stuck x) : detNext x = x

theorem DescriptiveComplexity.detNext_eq {A : Type} [FirstOrder.Language.stGraph.Structure A] {x y : A} (h : DetEdge x y) : detNext x = y

theorem DescriptiveComplexity.reflTransGen_detEdge_iff_iterate {A : Type} [FirstOrder.Language.stGraph.Structure A] (s t : A) : Relation.ReflTransGen DetEdge s t ↔ ∃ (n : ℕ), detNext^[n] s = t

Reachability along forced arcs is iteration of the successor map.

theorem DescriptiveComplexity.exists_iterate_detNext_lt_card {A : Type} [FirstOrder.Language.stGraph.Structure A] [Finite A] {s t : A} (h : ∃ (n : ℕ), detNext^[n] s = t) : ∃ n < Nat.card A, detNext^[n] s = t

The step budget: a vertex reachable along forced arcs is reachable in fewer steps than the universe has elements – the machine-free DescriptiveComplexity.exists_iterate_lt_card, read for the forced arcs.

The scanning walk

A node is a mode – false while scanning, true once done – together with a triple (s, x, c): the source candidate being tested, the current position of the walk, and the budget, itself a vertex, counted by its rank in the order.

noncomputable def DescriptiveComplexity.UnreachD.srcF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

u is a marked source, as a formula.

Equations

• DescriptiveComplexity.UnreachD.srcF u = FirstOrder.Language.sgSourceO.formula₁ (FirstOrder.Language.var u)

noncomputable def DescriptiveComplexity.UnreachD.tgtF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

u is a marked target, as a formula.

Equations

• DescriptiveComplexity.UnreachD.tgtF u = FirstOrder.Language.sgTargetO.formula₁ (FirstOrder.Language.var u)

noncomputable def DescriptiveComplexity.UnreachD.edgeF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

There is an arc from u to v, as a formula.

Equations

• DescriptiveComplexity.UnreachD.edgeF u v = FirstOrder.Language.sgEdgeO.formula₂ (FirstOrder.Language.var u) (FirstOrder.Language.var v)

noncomputable def DescriptiveComplexity.UnreachD.detEdgeF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

The arc from u to v is forced, as a formula: it is an arc, and it is the only one out of u.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.UnreachD.stuckF {γ : Type} (u : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

No arc out of u is forced, as a formula.

Equations

• DescriptiveComplexity.UnreachD.stuckF u = FirstOrder.Language.Formula.iAlls (Fin 1) (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.UnreachD.detEdgeF (Sum.inl u) (Sum.inr 0)))

def DescriptiveComplexity.UnreachD.eqF {γ : Type} (u v : γ) : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula γ

Equality of two variables, as a formula.

Equations

• DescriptiveComplexity.UnreachD.eqF u v = (FirstOrder.Language.var u).equal (FirstOrder.Language.var v)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_srcF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (srcF u).Realize v ↔ SGSource (v u)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_tgtF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (tgtF u).Realize v ↔ SGTarget (v u)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_edgeF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (edgeF u w).Realize v ↔ SGEdge (v u) (v w)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_eqF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (eqF u w).Realize v ↔ v u = v w

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_detEdgeF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u w : γ) : (detEdgeF u w).Realize v ↔ DetEdge (v u) (v w)

@[simp]

theorem DescriptiveComplexity.UnreachD.realize_stuckF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] {γ : Type} {v : γ → A} (u : γ) : (stuckF u).Realize v ↔ Stuck (v u)

The specification

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vS : Fin 3 ⊕ Fin 3

The current source candidate.

Equations

• DescriptiveComplexity.UnreachD.vS = Sum.inl 0

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vX : Fin 3 ⊕ Fin 3

The current position of the walk.

Equations

• DescriptiveComplexity.UnreachD.vX = Sum.inl 1

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vC : Fin 3 ⊕ Fin 3

The current budget.

Equations

• DescriptiveComplexity.UnreachD.vC = Sum.inl 2

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vS' : Fin 3 ⊕ Fin 3

The next source candidate.

Equations

• DescriptiveComplexity.UnreachD.vS' = Sum.inr 0

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vX' : Fin 3 ⊕ Fin 3

The next position.

Equations

• DescriptiveComplexity.UnreachD.vX' = Sum.inr 1

@[reducible, inline]

abbrev DescriptiveComplexity.UnreachD.vC' : Fin 3 ⊕ Fin 3

The next budget.

Equations

• DescriptiveComplexity.UnreachD.vC' = Sum.inr 2

noncomputable def DescriptiveComplexity.UnreachD.stepFF : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3 ⊕ Fin 3)

The transition of the scanning mode to itself: either follow the forced arc and spend one unit of budget, or – when the walk is stuck or the budget is exhausted – move on to the next source candidate. Both are guarded by the absence of a marked target ahead of a marked source, which is where the walk stops for good.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.UnreachD.stepFT : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3 ⊕ Fin 3)

The transition to the accepting mode: the last candidate has been scanned through.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.UnreachD.srcFml : (FirstOrder.Language.stGraph.sum FirstOrder.Language.order).Formula (Fin 3)

The starting nodes: the least candidate, the walk at that candidate, the full budget.

Equations

• DescriptiveComplexity.UnreachD.srcFml = DescriptiveComplexity.minF 0 ⊓ DescriptiveComplexity.UnreachD.eqF 1 0 ⊓ DescriptiveComplexity.minF 2

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.UnreachD.unreachdSpec : TCSpec FirstOrder.Language.stGraph

The specification whose deterministic walk scans for a forced path from a marked source to a marked target, accepting when it finds none.

Equations

• One or more equations did not get rendered due to their size.

Semantics of the walk

def DescriptiveComplexity.UnreachD.IsMinA {A : Type} [LinearOrder A] (a : A) : Prop

a is a least element of the order.

Equations

• DescriptiveComplexity.UnreachD.IsMinA a = ∀ (b : A), a ≤ b

def DescriptiveComplexity.UnreachD.IsMaxA {A : Type} [LinearOrder A] (a : A) : Prop

a is a greatest element of the order.

Equations

• DescriptiveComplexity.UnreachD.IsMaxA a = ∀ (b : A), b ≤ a

def DescriptiveComplexity.UnreachD.IsSuccA {A : Type} [LinearOrder A] (w z : A) : Prop

z covers w: the budget goes from w to z in one step.

Equations

• DescriptiveComplexity.UnreachD.IsSuccA w z = (w < z ∧ ∀ (a : A), ¬(w < a ∧ a < z))

def DescriptiveComplexity.UnreachD.UStep {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a b : Bool × (Fin 3 → A)) : Prop

One step of the scanning walk, in Lean: follow the forced arc while there is budget, otherwise move to the next candidate, or finish.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.UnreachD.realize_stepFF {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (x y : Fin 3 → A) : stepFF.Realize (Sum.elim x y) ↔ ¬(SGSource (x 0) ∧ SGTarget (x 1)) ∧ (y 0 = x 0 ∧ DetEdge (x 1) (y 1) ∧ IsSuccA (x 2) (y 2) ∨ (Stuck (x 1) ∨ IsMaxA (x 2)) ∧ IsSuccA (x 0) (y 0) ∧ y 1 = y 0 ∧ IsMinA (y 2))

theorem DescriptiveComplexity.UnreachD.realize_stepFT {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (x y : Fin 3 → A) : stepFT.Realize (Sum.elim x y) ↔ ¬(SGSource (x 0) ∧ SGTarget (x 1)) ∧ (Stuck (x 1) ∨ IsMaxA (x 2)) ∧ IsMaxA (x 0) ∧ IsMinA (y 0) ∧ IsMinA (y 1) ∧ IsMinA (y 2)

theorem DescriptiveComplexity.UnreachD.step_unreachdSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a b : unreachdSpec.Node A) : unreachdSpec.Step a b ↔ UStep a b

The walk of the specification is the scanning walk.

theorem DescriptiveComplexity.UnreachD.isSrc_unreachdSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a : unreachdSpec.Node A) : unreachdSpec.IsSrc a ↔ a.1 = false ∧ IsMinA (a.2 0) ∧ a.2 1 = a.2 0 ∧ IsMinA (a.2 2)

The starting nodes of the walk.

theorem DescriptiveComplexity.UnreachD.isTgt_unreachdSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a : unreachdSpec.Node A) : unreachdSpec.IsTgt a ↔ a.1 = true

The accepting nodes of the walk: those of the finished mode.

Order arithmetic for the budget

theorem DescriptiveComplexity.UnreachD.isMinA_unique {A : Type} [LinearOrder A] {a b : A} (ha : IsMinA a) (hb : IsMinA b) : a = b

theorem DescriptiveComplexity.UnreachD.isSuccA_unique {A : Type} [LinearOrder A] {c b b' : A} (h : IsSuccA c b) (h' : IsSuccA c b') : b = b'

theorem DescriptiveComplexity.UnreachD.not_isSuccA_of_isMaxA {A : Type} [LinearOrder A] {c b : A} (hc : IsMaxA c) (h : IsSuccA c b) : False

theorem DescriptiveComplexity.UnreachD.lt_or_eq_of_lt_isSuccA {A : Type} [LinearOrder A] {w z a : A} (h : IsSuccA w z) (ha : a < z) : a < w ∨ a = w

theorem DescriptiveComplexity.UnreachD.exists_isSuccA_of_not_isMaxA {A : Type} [LinearOrder A] [Finite A] {c : A} (h : ¬IsMaxA c) : ∃ (c' : A), IsSuccA c c'

theorem DescriptiveComplexity.UnreachD.orank_lt_card {A : Type} [LinearOrder A] [Finite A] (z : A) : orank z < Nat.card A

The rank of an element is smaller than the size of the universe: the budget allows exactly as many steps as there are elements, less one.

theorem DescriptiveComplexity.UnreachD.orank_of_isMinA {A : Type} [LinearOrder A] {a : A} (h : IsMinA a) : orank a = 0

theorem DescriptiveComplexity.UnreachD.orank_of_isSuccA {A : Type} [LinearOrder A] [Finite A] {w z : A} (h : IsSuccA w z) : orank z = orank w + 1

theorem DescriptiveComplexity.UnreachD.orank_of_isMaxA {A : Type} [LinearOrder A] [Finite A] {z : A} (h : IsMaxA z) : orank z = Nat.card A - 1

Determinism of the scanning walk

theorem DescriptiveComplexity.UnreachD.functional_unreachdSpec {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] : unreachdSpec.Functional A

The scanning walk is deterministic.

Correctness of the scan

def DescriptiveComplexity.UnreachD.Bad {A : Type} [FirstOrder.Language.stGraph.Structure A] (s : A) : Prop

A marked source with a marked target ahead of it: what the scan looks for, and what its acceptance denies.

Equations

• DescriptiveComplexity.UnreachD.Bad s = (DescriptiveComplexity.SGSource s ∧ ∃ (t : A), DescriptiveComplexity.SGTarget t ∧ Relation.ReflTransGen DescriptiveComplexity.DetEdge s t)

theorem DescriptiveComplexity.UnreachD.detReachable_iff_exists_bad {A : Type} [FirstOrder.Language.stGraph.Structure A] : DetReachable A ↔ ∃ (s : A), Bad s

theorem DescriptiveComplexity.UnreachD.iterate_of_stuck {A : Type} [FirstOrder.Language.stGraph.Structure A] {x : A} (h : Stuck x) (n : ℕ) : detNext^[n] x = x

def DescriptiveComplexity.UnreachD.Inv {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] (a : Bool × (Fin 3 → A)) : Prop

The invariant carried along the scan: every candidate already passed is harmless, and if the current one is not, its target is still ahead of the walk and within the remaining budget.

Equations

• One or more equations did not get rendered due to their size.

theorem DescriptiveComplexity.UnreachD.not_bad_of_end {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a : Bool × (Fin 3 → A)} (hguard : ¬(SGSource (a.2 0) ∧ SGTarget (a.2 1))) (hend : Stuck (a.2 1) ∨ IsMaxA (a.2 2)) (hinv : Bad (a.2 0) → ∃ (t : A) (n : ℕ), SGTarget t ∧ n + orank (a.2 2) < Nat.card A ∧ detNext^[n] (a.2 1) = t) : ¬Bad (a.2 0)

At the end of an inner loop – the walk stuck, or the budget spent – the current candidate is harmless: its target would have to be where the walk already stands, and the walk has not stopped there.

theorem DescriptiveComplexity.UnreachD.inv_step {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a b : Bool × (Fin 3 → A)} (h : UStep a b) (hinv : Inv a) : Inv b

The invariant is preserved by every step of the scan.

theorem DescriptiveComplexity.UnreachD.inv_reach {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {a b : unreachdSpec.Node A} (h : unreachdSpec.Reach a b) (hinv : Inv a) : Inv b

theorem DescriptiveComplexity.UnreachD.inv_of_isSrc {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] {a : unreachdSpec.Node A} (h : unreachdSpec.IsSrc a) : Inv a

The starting node satisfies the invariant: nothing has been scanned, and the whole universe is still available as budget.

theorem DescriptiveComplexity.UnreachD.not_detReachable_of_accepts {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (h : unreachdSpec.Accepts A) : ¬DetReachable A

Soundness: if the scan finishes, there was nothing to find.

Completeness of the scan

Nothing to find means nothing stops the walk, so it runs the inner loop to its end for every candidate and finishes.

theorem DescriptiveComplexity.UnreachD.reach_of_inner {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] (hnb : ∀ (s : A), ¬Bad s) (s : A) (z : Bool × (Fin 3 → A)) (hz : ∀ (x c : A), Relation.ReflTransGen DetEdge s x → Stuck x ∨ IsMaxA c → UStep (false, ![s, x, c]) z) (m : ℕ) (c x : A) : Nat.card A - orank c ≤ m → Relation.ReflTransGen DetEdge s x → unreachdSpec.Reach (false, ![s, x, c]) z

The inner loop: from any position of the walk on the candidate s, with any budget, the node z that ends the loop is reached.

theorem DescriptiveComplexity.UnreachD.reach_candidate {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] (hnb : ∀ (s : A), ¬Bad s) {a₀ : A} (h₀ : IsMinA a₀) (s : A) : unreachdSpec.Reach (false, ![a₀, a₀, a₀]) (false, ![s, s, a₀])

The outer loop: every candidate is reached, in the order of the structure.

theorem DescriptiveComplexity.UnreachD.accepts_of_not_detReachable {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] (h : ¬DetReachable A) : unreachdSpec.Accepts A

Completeness: if there is nothing to find, the scan finishes.

theorem DescriptiveComplexity.UnreachD.accepts_unreachdSpec_iff {A : Type} [FirstOrder.Language.stGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : unreachdSpec.Accepts A ↔ ¬DetReachable A

The scan decides non-reachability along forced arcs.

UNREACHd, and the closure of LOGSPACE under complement

theorem DescriptiveComplexity.unreachd_dtcDefinable : DTCDefinable REACHdᶜ

The complement of REACHd is FO(DTC) definable: the scan is deterministic (DescriptiveComplexity.UnreachD.functional_unreachdSpec), so its determinization is itself, and it accepts exactly the marked graphs in which no marked target lies ahead of a marked source.

theorem DescriptiveComplexity.dtcDefinable_compl {L : FirstOrder.Language} {P : DecisionProblem L} (h : DTCDefinable P) : DTCDefinable Pᶜ

FO(DTC) definability is closed under complement. The complement of P reduces to the complement of REACHd – a reduction complements along with its two problems – and that complement is FO(DTC) definable.

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

Membership in LOGSPACE is closed under complement.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.coLOGSPACE : ComplexityClass

coLOGSPACE, the complement class of LOGSPACE. That it is LOGSPACE is DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE.

Equations

• DescriptiveComplexity.coLOGSPACE = DescriptiveComplexity.LOGSPACE.compl

theorem DescriptiveComplexity.LOGSPACE_eq_coLOGSPACE : LOGSPACE = coLOGSPACE

L = coL: deterministic logarithmic space is closed under complement. Unlike NL = coNL (DescriptiveComplexity.NL_eq_coNL, Immerman–Szelepcsényi) this needs no inductive counting: a deterministic walk has only one thing to do at each node, so not arriving is witnessed by walking until the budget runs out.

def DescriptiveComplexity.UNREACHd : DecisionProblem FirstOrder.Language.stGraph

UNREACHd, the complement of REACHd: no marked target is reachable from a marked source along forced arcs.

Equations

• DescriptiveComplexity.UNREACHd = DescriptiveComplexity.REACHdᶜ

theorem DescriptiveComplexity.unreachd_mem_LOGSPACE : LOGSPACE.Mem UNREACHd

UNREACHd is in LOGSPACE, by the scan.

theorem DescriptiveComplexity.unreachd_LOGSPACE_hard : LOGSPACE.Hard UNREACHd

UNREACHd is LOGSPACE-hard, by complementing the discharge: the complement of a problem of the class is again in the class, it reduces to REACHd, and the very same interpretation reduces the problem itself to UNREACHd.

theorem DescriptiveComplexity.UNREACHd_LOGSPACE_complete : LOGSPACE.Complete UNREACHd

UNREACHd is LOGSPACE-complete. Both halves come from the same side here, unlike the REACH/UNREACH pair one level up: an operator-based logic defines a problem and its complement alike, so no analogue of Immerman–Szelepcsényi is needed to complete the picture.