First-order reductions and projections

A first-order reduction between decision problems (Boolean queries over finite structures) is a first-order interpretation: the target structure is defined from the source by FO formulas, one per target relation symbol. This module gives the dimension-1 (universe-preserving) case — each target relation is an FO-definable relation on the same universe — the foundational special case of the general dimension-k interpretation (whose target universe is a definable subset of domᵏ, recorded as a roadmap L6 milestone).

First-order reductions are the reductions of descriptive complexity: weak enough to sit inside FO/AC⁰, yet enough to define completeness for the standard classes. Their quantifier-free restriction — first-order projections — is weaker still and is the notion under which many natural problems are complete.

Each Boolean query induces a machine-model Language via queryLanguage; the string-level FO-reduction (an FO map on encodings) is a further step on track L6.

Main definitions and results

• FOInterpretation — a dimension-1 first-order interpretation V → W.
• FOInterpretation.apply — the induced structure map, with apply_idInterp.
• FOReduces — first-order reducibility between Boolean queries, with reflexivity and transitivity.
• FOInterpretation.IsQuantifierFree, FOProjReduces — first-order projections, with FOInterpretation.IsQuantifierFree.comp, FOProjReduces.toFOReduces, and reflexivity/transitivity.

structure Complexity.DescriptiveComplexity.FOInterpretation (V W : Vocabulary) : Type

A (dimension-1) first-order interpretation from vocabulary V to W: each target relation symbol is defined by an FO formula over V with one free variable per argument, and each target constant symbol is a source constant. Applying it to a V-structure yields a W-structure on the same universe.

• relFormula (i : Fin W.numRels) : Formula V (W.relArity i)

  The FO formula (over V) defining each target relation of W.

• constMap : Fin W.numConsts → Fin V.numConsts

  Each target constant of W is interpreted as a source constant of V.

def Complexity.DescriptiveComplexity.FOInterpretation.apply {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) : FinStruct W

Apply an interpretation to a source structure, producing a target structure on the same universe: each target relation holds exactly when its defining formula does.

Equations

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

def Complexity.DescriptiveComplexity.FOInterpretation.idInterp (V : Vocabulary) : FOInterpretation V V

The identity interpretation: each relation is defined by its own atom R(x₀, …, x_{a-1}) and each constant maps to itself.

Equations

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

theorem Complexity.DescriptiveComplexity.FOInterpretation.apply_idInterp {V : Vocabulary} (A : FinStruct V) : (idInterp V).apply A = A

The identity interpretation acts as the identity on structures.

def Complexity.DescriptiveComplexity.FOInterpretation.translateTerm {V W : Vocabulary} {n : Nat} (I : FOInterpretation V W) : Term W n → Term V n

Translate a W-term to a V-term along the interpretation: a variable stays put, and a target constant becomes its designated source constant.

Equations

• I.translateTerm (Complexity.DescriptiveComplexity.Term.var j) = Complexity.DescriptiveComplexity.Term.var j
• I.translateTerm (Complexity.DescriptiveComplexity.Term.const c) = Complexity.DescriptiveComplexity.Term.const (I.constMap c)

theorem Complexity.DescriptiveComplexity.FOInterpretation.translateTerm_eval {V W : Vocabulary} {n : Nat} (I : FOInterpretation V W) (A : FinStruct V) (σ : Env A.card n) (t : Term W n) : Term.eval A σ (I.translateTerm t) = Term.eval (I.apply A) σ t

Term-level transport. Evaluating a translated term in the source structure agrees with evaluating the original term in the interpreted structure. This is the base case of the full (formula-level) transport theorem.

theorem Complexity.DescriptiveComplexity.FOInterpretation.apply_rel {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) (i : Fin W.numRels) (args : Fin (W.relArity i) → Fin A.card) : (I.apply A).rel i args = Formula.Sat A args (I.relFormula i)

The interpreted structure's relation is (definitionally) satisfaction of the defining formula.

def Complexity.DescriptiveComplexity.FOInterpretation.translate {V W : Vocabulary} (I : FOInterpretation V W) {n : Nat} : Formula W n → Formula V n

Translate a W-formula to a V-formula along the interpretation: a target relation atom is replaced by its defining formula with the (translated) argument terms substituted in; other connectives and quantifiers are traversed.

Equations

• I.translate (Complexity.DescriptiveComplexity.Formula.relApp i ts) = (I.relFormula i).subst fun (k : Fin (W.relArity i)) => I.translateTerm (ts k)
• I.translate (Complexity.DescriptiveComplexity.Formula.eq t₁ t₂) = Complexity.DescriptiveComplexity.Formula.eq (I.translateTerm t₁) (I.translateTerm t₂)
• I.translate φ.neg = (I.translate φ).neg
• I.translate (φ.conj ψ) = (I.translate φ).conj (I.translate ψ)
• I.translate (φ.disj ψ) = (I.translate φ).disj (I.translate ψ)
• I.translate φ.exist = (I.translate φ).exist
• I.translate φ.all = (I.translate φ).all

theorem Complexity.DescriptiveComplexity.FOInterpretation.translate_sat {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) {n : Nat} (σ : Env A.card n) (φ : Formula W n) : Formula.Sat (I.apply A) σ φ ↔ Formula.Sat A σ (I.translate φ)

The transport theorem (fundamental theorem of interpretations). Satisfaction of a formula in the interpreted structure I.apply A equals satisfaction of its translation in the source structure A. This is what makes FO-reductions compose.

def Complexity.DescriptiveComplexity.FOInterpretation.comp {V W U : Vocabulary} (I₂ : FOInterpretation V W) (I₁ : FOInterpretation U V) : FOInterpretation U W

Compose two interpretations by translating the outer defining formulas through the inner interpretation (I₂ ∘ I₁, source U → V → W).

Equations

• I₂.comp I₁ = { relFormula := fun (i : Fin W.numRels) => I₁.translate (I₂.relFormula i), constMap := fun (c : Fin W.numConsts) => I₁.constMap (I₂.constMap c) }

theorem Complexity.DescriptiveComplexity.FOInterpretation.apply_comp {V W U : Vocabulary} (I₂ : FOInterpretation V W) (I₁ : FOInterpretation U V) (A : FinStruct U) : (I₂.comp I₁).apply A = I₂.apply (I₁.apply A)

Composition applies as composition of structure maps: (I₂ ∘ I₁).apply A = I₂.apply (I₁.apply A). The relation fields agree by the transport theorem.

def Complexity.DescriptiveComplexity.FOReduces {V W : Vocabulary} (Q₁ : BooleanQuery V) (Q₂ : BooleanQuery W) : Prop

First-order reduction between Boolean queries: an FO-interpretation carrying Q₁-membership to Q₂-membership on the interpreted structure.

Equations

• Complexity.DescriptiveComplexity.FOReduces Q₁ Q₂ = ∃ (I : Complexity.DescriptiveComplexity.FOInterpretation V W), ∀ (A : Complexity.DescriptiveComplexity.FinStruct V), Q₁ A ↔ Q₂ (I.apply A)

theorem Complexity.DescriptiveComplexity.FOReduces.refl {V : Vocabulary} (Q : BooleanQuery V) : FOReduces Q Q

FO-reducibility is reflexive, via the identity interpretation.

theorem Complexity.DescriptiveComplexity.FOReduces.complement {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOReduces Q₁ Q₂) : FOReduces Q₁.complement Q₂.complement

First-order reductions respect complementation: the same interpretation witnesses Q₁ᶜ ≤ Q₂ᶜ, since the carrying biconditional negates.

theorem Complexity.DescriptiveComplexity.FOReduces.trans {V W U : Vocabulary} {Q₁ : BooleanQuery U} {Q₂ : BooleanQuery V} {Q₃ : BooleanQuery W} (h₁ : FOReduces Q₁ Q₂) (h₂ : FOReduces Q₂ Q₃) : FOReduces Q₁ Q₃

FO-reducibility is transitive, via composition of interpretations (the transport theorem is exactly what makes the composite carry membership). Together with FOReduces.refl, FO-reducibility is a preorder on Boolean queries.

def Complexity.DescriptiveComplexity.FOInterpretation.IsQuantifierFree {V W : Vocabulary} (I : FOInterpretation V W) : Prop

An interpretation is quantifier-free when every defining formula has quantifier rank 0 — the coarse form of a first-order projection.

Equations

• I.IsQuantifierFree = ∀ (i : Fin W.numRels), (I.relFormula i).quantifierRank = 0

theorem Complexity.DescriptiveComplexity.FOInterpretation.IsQuantifierFree.quantifierRank_translate {V W : Vocabulary} {I : FOInterpretation V W} (hI : I.IsQuantifierFree) {n : Nat} (φ : Formula W n) : (I.translate φ).quantifierRank = φ.quantifierRank

Translating through a quantifier-free interpretation preserves quantifier rank. Relation atoms are replaced by quantifier-free defining formulas, while all logical connectives and quantifiers retain their original structure.

theorem Complexity.DescriptiveComplexity.FOInterpretation.idInterp_isQuantifierFree {V : Vocabulary} : (idInterp V).IsQuantifierFree

The identity interpretation is quantifier-free (each relation is a bare atom).

theorem Complexity.DescriptiveComplexity.FOInterpretation.IsQuantifierFree.comp {V W U : Vocabulary} {I₂ : FOInterpretation V W} {I₁ : FOInterpretation U V} (hI₂ : I₂.IsQuantifierFree) (hI₁ : I₁.IsQuantifierFree) : (I₂.comp I₁).IsQuantifierFree

Composing quantifier-free interpretations remains quantifier-free.

def Complexity.DescriptiveComplexity.FOProjReduces {V W : Vocabulary} (Q₁ : BooleanQuery V) (Q₂ : BooleanQuery W) : Prop

A first-order projection reduction: an FO-reduction witnessed by a quantifier-free interpretation.

Equations

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

theorem Complexity.DescriptiveComplexity.FOProjReduces.toFOReduces {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (h : FOProjReduces Q₁ Q₂) : FOReduces Q₁ Q₂

Every first-order projection is in particular a first-order reduction.

theorem Complexity.DescriptiveComplexity.FOProjReduces.refl {V : Vocabulary} (Q : BooleanQuery V) : FOProjReduces Q Q

FO-projection reducibility is reflexive, via the (quantifier-free) identity.

theorem Complexity.DescriptiveComplexity.FOProjReduces.trans {V W U : Vocabulary} {Q₁ : BooleanQuery U} {Q₂ : BooleanQuery V} {Q₃ : BooleanQuery W} (h₁ : FOProjReduces Q₁ Q₂) (h₂ : FOProjReduces Q₂ Q₃) : FOProjReduces Q₁ Q₃

FO-projection reducibility is transitive. Composition preserves both the query-membership equivalence and quantifier-freeness of the interpretation.