Relativized first-order interpretations (definable target universes)

An DescriptiveComplexity.FOInterpretation fixes the target universe to all of Tag × A^dim. That is convenient for subset-style problems – a yes-witness lives on part of the universe and junk elements sit isolated and unused – but it cannot target a spanning problem such as HAMILTON CIRCUIT, where a yes-witness (a tour) must visit every universe element: junk points with no valid incident edges make every interpreted instance a no-instance.

The textbook remedy (Immerman 1999) is a domain formula: the target universe is a definable subset of Tag × A^dim. This file adds it as a layer on top of FOInterpretation, so that no existing interpretation, reduction or problem file changes:

• DescriptiveComplexity.RelFOInterpretation extends FOInterpretation with a domFormula : Tag → L.Formula (Fin dim);
• DescriptiveComplexity.RelFOInterpretation.MapRel is the interpreted structure carried by the subtype {x : Tag × A^dim // domFormula holds of x};
• DescriptiveComplexity.RelOrderedFOReduction (notation ≤ʳᶠᵒ[≤]) is the ordered reduction through such an interpretation, carrying the extra obligation dom_nonempty – a definable domain can be empty on a nonempty structure, so Nonempty Tag no longer guarantees a nonempty output;
• DescriptiveComplexity.OrderedFOReduction.toRel embeds an ordinary ordered reduction as a relativized one with domFormula := ⊤, the transparency of the whole-universe case being an isomorphism (DescriptiveComplexity.FOInterpretation.toRelLEquiv) rather than a definitional equality.

This is the hardness-side machinery of relativized reductions; it is what a hardness proof for a spanning problem needs. Membership closure under relativized reductions is deferred, and not needed when membership is a direct second-order sentence.

structure DescriptiveComplexity.RelFOInterpretation (L L' : FirstOrder.Language) (Tag : Type) (dim : ℕ) extends DescriptiveComplexity.FOInterpretation L L' Tag dim : Type

A relativized tagged first-order interpretation: an ordinary interpretation together with, for each tag, a domain formula on the dim coordinates. The target universe is cut down to the tagged tuples whose coordinates satisfy their tag's domain formula.

• relFormula {n : ℕ} : L'.Relations n → (Fin n → Tag) → L.Formula (Fin n × Fin dim)
• domFormula : Tag → L.Formula (Fin dim)

  The domain formula of each tag: a tagged tuple (t, ā) belongs to the target universe iff domFormula t holds of ā.

def DescriptiveComplexity.RelFOInterpretation.MapRel {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A] : Type

The universe of the relativized interpretation in A: the tagged tuples whose coordinates satisfy their tag's domain formula. A subtype (not a def of a product) so that the definable restriction is real; the L'-structure on it reads its relations through Subtype.val, exactly as FOInterpretation.Map does.

Equations

• I.MapRel A = { x : Tag × (Fin dim → A) // (I.domFormula x.1).Realize x.2 }

@[instance_reducible]

instance DescriptiveComplexity.RelFOInterpretation.mapRelStructure {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A] [L'.IsRelational] : L'.Structure (I.MapRel A)

The L'-structure interpreted on the definable subset.

Equations

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

theorem DescriptiveComplexity.RelFOInterpretation.relMap_mapRel {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A] [L'.IsRelational] {n : ℕ} (R : L'.Relations n) (xs : Fin n → I.MapRel A) : FirstOrder.Language.Structure.RelMap R xs ↔ (I.relFormula R fun (i : Fin n) => (↑(xs i)).1).Realize fun (p : Fin n × Fin dim) => (↑(xs p.1)).2 p.2

theorem DescriptiveComplexity.RelFOInterpretation.mapRel_finite {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A] [Finite Tag] [Finite A] : Finite (I.MapRel A)

The relativized universe of a finite structure over finite tags is finite.

Functoriality on isomorphisms

def DescriptiveComplexity.RelFOInterpretation.mapRelLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} [L'.IsRelational] (I : RelFOInterpretation L L' Tag dim) {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : L'.Equiv (I.MapRel M) (I.MapRel N)

Relativized interpretations are functorial on L-isomorphisms: the domain formula is an L-formula, so its truth transports, and the induced map of subtypes is an L'-isomorphism.

Equations

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

The whole-universe case is an ordinary interpretation

def DescriptiveComplexity.FOInterpretation.toRel {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : FOInterpretation L L' Tag dim) : RelFOInterpretation L L' Tag dim

Any interpretation is a relativized one whose domain formula is ⊤: the target universe is all of Tag × A^dim, as before.

Equations

• I.toRel = { toFOInterpretation := I, domFormula := fun (x : Tag) => ⊤ }

def DescriptiveComplexity.FOInterpretation.toRelLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} [L'.IsRelational] (I : FOInterpretation L L' Tag dim) (A : Type) [L.Structure A] : L'.Equiv (I.Map A) (I.toRel.MapRel A)

The transparency of the ⊤ domain: the relativized universe of I.toRel is L'-isomorphic to the ordinary universe of I. (Not a definitional equality – a subtype over ⊤ is not the product on the nose.)

Equations

• I.toRelLEquiv A = { toFun := fun (a : I.Map A) => ⟨a, ⋯⟩, invFun := fun (x : I.toRel.MapRel A) => ↑x, left_inv := ⋯, right_inv := ⋯, map_fun' := ⋯, map_rel' := ⋯ }

Relativized ordered reductions

structure DescriptiveComplexity.RelOrderedFOReduction {L L' : FirstOrder.Language} [L'.IsRelational] (P : DecisionProblem L) (Q : DecisionProblem L') : Type 1

An ordered first-order reduction through a relativized interpretation: like DescriptiveComplexity.OrderedFOReduction, but the target universe is the definable subset carved out by the domain formula. The Nonempty Tag field of the ordinary reduction is replaced by dom_nonempty, since a definable domain may be empty even when the tags and the input are not.

• Tag : Type

  The tags used by the underlying interpretation.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures map to finite structures.

• dim : ℕ

  The dimension of the underlying interpretation.

• toRelInterpretation : RelFOInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim

  The underlying relativized interpretation, over the ordered expansion.

• dom_nonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : ∃ (t : self.Tag) (w : Fin self.dim → A), (self.toRelInterpretation.domFormula t).Realize w

  The definable domain is inhabited: some tagged tuple satisfies its tag's domain formula. This replaces Nonempty Tag, which no longer suffices.

• correct (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : P.Holds A ↔ Q.Holds (self.toRelInterpretation.MapRel A)

  Yes-instances map exactly to yes-instances, whatever the linear order.

def DescriptiveComplexity.«term_≤ʳᶠᵒ[≤]_» : Lean.TrailingParserDescr

An ordered first-order reduction through a relativized interpretation: like DescriptiveComplexity.OrderedFOReduction, but the target universe is the definable subset carved out by the domain formula. The Nonempty Tag field of the ordinary reduction is replaced by dom_nonempty, since a definable domain may be empty even when the tags and the input are not.

Equations

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

theorem DescriptiveComplexity.RelOrderedFOReduction.mapRel_nonempty {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : RelOrderedFOReduction P Q) (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty (f.toRelInterpretation.MapRel A)

The relativized universe of the output of a reduction is nonempty on nonempty finite ordered inputs.

def DescriptiveComplexity.OrderedFOReduction.toRel {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) : RelOrderedFOReduction P Q

An ordinary ordered FO reduction is a relativized one with ⊤ domain: the correctness is transported across DescriptiveComplexity.FOInterpretation.toRelLEquiv, and the domain is inhabited by any tag and any constant tuple.

Equations

• f.toRel = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toRelInterpretation := f.toInterpretation.toRel, dom_nonempty := ⋯, correct := ⋯ }

def DescriptiveComplexity.RelOrderedFOReduction.congrSource {L L' : FirstOrder.Language} [L'.IsRelational] {P P' : DecisionProblem L} {S : DecisionProblem L'} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ P'.Holds A) (g : RelOrderedFOReduction P S) : RelOrderedFOReduction P' S

A relativized reduction can be transported along an agreement of the source problems on finite structures.

Equations

• DescriptiveComplexity.RelOrderedFOReduction.congrSource h g = { Tag := g.Tag, tagFinite := ⋯, dim := g.dim, toRelInterpretation := g.toRelInterpretation, dom_nonempty := ⋯, correct := ⋯ }