Reductions by tagged first-order interpretations

A reduction supplies a tagged full-product interpretation and a proof that it preserves membership. Invariance of the target problem turns the composition isomorphism into transitivity. The resulting reducibility relation is a preorder, respects complement, and preserves first-order definability downwards.

This is the tagged version of the structural reductions in Immerman, Chapter 3, and Senellart--Gnatenko (2026), Sections 3.1--3.2. It does not assert a resource bound for a map on binary encodings, nor the restricted syntax of an exact first-order projection.

structure Complexity.DescriptiveComplexity.TaggedFOReduction {V W : Vocabulary} (P : DecisionProblem V) (Q : DecisionProblem W) : Type

A first-order reduction with a fixed finite set of tags and a tuple dimension.

• tags : ℕ

  Number of disjoint copies of the tuple universe.

• dim : ℕ

  Number of source coordinates per target element.

• interpretation : TaggedFOInterpretation V W self.tags self.dim

  The first-order interpretation producing the target structure.

• correct (A : FinStruct V) : P.toQuery A ↔ Q.toQuery (self.interpretation.apply A)

  The interpretation preserves and reflects membership.

def Complexity.DescriptiveComplexity.TaggedFOReduction.refl {V : Vocabulary} (P : DecisionProblem V) : TaggedFOReduction P P

The identity interpretation is a reduction of a problem to itself.

Equations

• Complexity.DescriptiveComplexity.TaggedFOReduction.refl P = { tags := 1, dim := 1, interpretation := Complexity.DescriptiveComplexity.TaggedFOInterpretation.idInterp V, correct := ⋯ }

def Complexity.DescriptiveComplexity.TaggedFOReduction.trans {U V W : Vocabulary} {P : DecisionProblem U} {Q : DecisionProblem V} {R : DecisionProblem W} (f : TaggedFOReduction P Q) (g : TaggedFOReduction Q R) : TaggedFOReduction P R

Compose reductions by flattening their tags and coordinate tuples.

Equations

• f.trans g = { tags := g.tags * f.tags ^ g.dim, dim := g.dim * f.dim, interpretation := g.interpretation.comp f.interpretation, correct := ⋯ }

def Complexity.DescriptiveComplexity.TaggedFOReduction.complement {V W : Vocabulary} {P : DecisionProblem V} {Q : DecisionProblem W} (f : TaggedFOReduction P Q) : TaggedFOReduction P.complement Q.complement

The same interpretation reduces the two complementary problems.

Equations

• f.complement = { tags := f.tags, dim := f.dim, interpretation := f.interpretation, correct := ⋯ }

def Complexity.DescriptiveComplexity.TaggedFOReduces {V W : Vocabulary} (P : DecisionProblem V) (Q : DecisionProblem W) : Prop

Reducibility by a tagged full-product first-order interpretation.

Equations

• Complexity.DescriptiveComplexity.TaggedFOReduces P Q = Nonempty (Complexity.DescriptiveComplexity.TaggedFOReduction P Q)

theorem Complexity.DescriptiveComplexity.TaggedFOReduces.refl {V : Vocabulary} (P : DecisionProblem V) : TaggedFOReduces P P

Tagged first-order reducibility is reflexive.

theorem Complexity.DescriptiveComplexity.TaggedFOReduces.trans {U V W : Vocabulary} {P : DecisionProblem U} {Q : DecisionProblem V} {R : DecisionProblem W} (h₁ : TaggedFOReduces P Q) (h₂ : TaggedFOReduces Q R) : TaggedFOReduces P R

Tagged first-order reducibility is transitive, even across vocabularies.

theorem Complexity.DescriptiveComplexity.TaggedFOReduces.complement {V W : Vocabulary} {P : DecisionProblem V} {Q : DecisionProblem W} (h : TaggedFOReduces P Q) : TaggedFOReduces P.complement Q.complement

Tagged first-order reducibility respects complementation.

@[instance_reducible]

def Complexity.DescriptiveComplexity.TaggedFOReduces.preorder (V : Vocabulary) : Preorder (DecisionProblem V)

The preorder on problems over one vocabulary, available without a global order instance.

Equations

• Complexity.DescriptiveComplexity.TaggedFOReduces.preorder V = { le := Complexity.DescriptiveComplexity.TaggedFOReduces, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Complexity.DescriptiveComplexity.FOReduces.toTaggedFOReduces {V W : Vocabulary} {P : DecisionProblem V} {Q : DecisionProblem W} (h : FOReduces P.toQuery Q.toQuery) : TaggedFOReduces P Q

Every universe-preserving reduction between invariant problems gives a tagged reduction.

theorem Complexity.DescriptiveComplexity.FODefinable.of_taggedReduces {V W : Vocabulary} {P : DecisionProblem V} {Q : DecisionProblem W} (hQ : FODefinable Q.toQuery) (h : TaggedFOReduces P Q) : FODefinable P.toQuery

FO definability is closed downwards under tagged first-order reductions.