FO(TC) reductions are strictly stronger than first-order ones

DescriptiveComplexity.FOReduction.toTC embeds every first-order reduction into the FO(TC) ones. The embedding is strict, and unconditionally: DescriptiveComplexity.EVEN reduces in FO(≤, TC) to a problem it does not reduce to first-order at all (DescriptiveComplexity.exists_tcReduction_not_orderedReduction).

The witness is the one of DescriptiveComplexity.FixedPointReductionStrict, now at the weakest reduction notion that can carry it: the target is DescriptiveComplexity.NONEMPTYMARK, “some element is marked”, which is first-order definable, so nothing first-order-reducing to it can escape first-order logic – and EVEN does (DescriptiveComplexity.even_not_foDefinable). The reduction marks every element when the universe is even and none when it is odd, and the walk that decides which is the one already in the catalog (DescriptiveComplexity.evenSpec: step to the successor, flip a bit), read as an atom through DescriptiveComplexity.TCSpec.acceptsF.

Since an FO(TC) reduction is an FO(LFP) reduction, this strengthens the separation of DescriptiveComplexity.FixedPointReductionStrict: the gap between ≤ᶠᵒ[≤] and ≤ˡᶠᵖ opens already at the logarithmic-space notion, and needs neither a fixed point nor a hard problem – only a walk along the order.

The last section sharpens it once more. The parity walk is functional – the mode flips and the immediate successor is unique (DescriptiveComplexity.evenSpec_functional) – so it survives determinization, and the separation holds already for the deterministic logarithmic-space reductions (DescriptiveComplexity.exists_dtcReduction_not_orderedReduction), which is the reduction notion of the textbooks. The same observation gives EVEN its FO(DTC) definition (DescriptiveComplexity.even_dtcDefinable), and so its membership in DescriptiveComplexity.LOGSPACE by the logic rather than through the bit-level stack.

The interpretation

noncomputable def DescriptiveComplexity.evenMarkTCInterp : TCInterpretation (FirstOrder.Language.empty.sum FirstOrder.Language.order) FirstOrder.Language.markedSet Unit 1

The FO(TC) interpretation reducing EVEN to DescriptiveComplexity.NONEMPTYMARK: the universe unchanged, every element marked exactly when the parity walk accepts.

Equations

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

theorem DescriptiveComplexity.relMap_evenMarkTCInterp (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] (xs : Fin 1 → evenMarkTCInterp.Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.markedSetMark xs ↔ evenSpec.Accepts A

Every point of the interpreted universe is marked exactly when the parity walk accepts.

theorem DescriptiveComplexity.evenMarkTCInterp_nonempty (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] [Nonempty A] : Nonempty (evenMarkTCInterp.Map A)

The interpreted universe is all of the base universe: the domain formula is ⊤.

The reduction and the separation

theorem DescriptiveComplexity.even_tcReduction_nonemptyMark : Nonempty (TCReduction EVEN NONEMPTYMARK)

EVEN FO(TC)-reduces to NONEMPTYMARK: one walk along the order decides the parity of the universe, and the reduction marks everything or nothing accordingly.

theorem DescriptiveComplexity.exists_tcReduction_not_orderedReduction : ∃ (L : FirstOrder.Language) (x : L.IsRelational) (Q : DecisionProblem L), Nonempty (TCReduction EVEN Q) ∧ IsEmpty (OrderedFOReduction EVEN Q)

FO(TC) reductions are strictly stronger than first-order ones, with EVEN as the witness: it reduces to DescriptiveComplexity.NONEMPTYMARK in FO(≤, TC) and by no first-order reduction. No complexity-theoretic assumption enters either half.

The walk is deterministic, so the separation is one notion lower

theorem DescriptiveComplexity.evenSpec_functional (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] : evenSpec.Functional A

The parity walk is functional: a node has at most one successor – the mode flips, and an element covers at most one element in a linear order.

theorem DescriptiveComplexity.reach_det_evenSpec_iff (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] (a b : evenSpec.Node A) : evenSpec.det.Reach a b ↔ evenSpec.Reach a b

Determinization does not change what the parity walk reaches.

theorem DescriptiveComplexity.accepts_det_evenSpec_iff (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] : evenSpec.det.Accepts A ↔ evenSpec.Accepts A

The deterministic reading of the parity walk accepts exactly when the walk does: determinization changes nothing on a functional walk.

theorem DescriptiveComplexity.even_dtcDefinable : DTCDefinable EVEN

EVEN is FO(DTC) definable: the parity walk is deterministic, so the walk that defines EVEN survives Immerman's determinization. Hence EVEN is in DescriptiveComplexity.LOGSPACE by the logic, the bit-level route (DescriptiveComplexity.even_mem_LOGSPACE_bit) being a second proof.

theorem DescriptiveComplexity.evenSpec_toParam_functional (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] : evenSpec.toParam.Functional A

The parity walk, as a parameterized walk, is functional too.

theorem DescriptiveComplexity.evenSpec_toFamily_functional (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] : evenSpec.toFamily.Functional A

The one-element family of the parity walk is functional.

theorem DescriptiveComplexity.relMap_evenMarkDetInterp (A : Type) [FirstOrder.Language.empty.Structure A] [LinearOrder A] (xs : Fin 1 → { fam := evenSpec.toFamily.det, toRel := evenMarkTCInterp.toRel }.Map A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.markedSetMark xs ↔ evenSpec.Accepts A

Every point of the interpreted universe is marked exactly when the determinized parity walk accepts – which, the walk being functional, is when the universe is even.

theorem DescriptiveComplexity.even_dtcReduction_nonemptyMark : Nonempty (DTCReduction EVEN NONEMPTYMARK)

EVEN reduces to NONEMPTYMARK by a deterministic logarithmic-space reduction: the walk that decides the parity of the universe follows, from each element, its unique successor.

theorem DescriptiveComplexity.exists_dtcReduction_not_orderedReduction : ∃ (L : FirstOrder.Language) (x : L.IsRelational) (Q : DecisionProblem L), Nonempty (DTCReduction EVEN Q) ∧ IsEmpty (OrderedFOReduction EVEN Q)

Deterministic logarithmic-space reductions are already strictly stronger than first-order ones: EVEN reduces to DescriptiveComplexity.NONEMPTYMARK in FO(≤, DTC) – one walk that never has a choice – and by no first-order reduction. This is the sharpest form of the separation: the notion on the left is the many-one reduction of the textbooks.