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.

The reduction and the separation

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.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. Registered in the Lax archive as Lax945089.FirstOrderBelowTransitiveClosure.even_dtcDefinable.

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. Registered in the Lax archive as Lax945089.ReductionsBelowLogSpace.exists_dtcReduction_not_orderedReduction.