The power interpretation on k-tuples

Given a finite relational vocabulary v : Vocabulary L and a tuple width k ≥ 1 bounding all arities of v, a k-tuple x : Fin k → M over a finite structure M numbered by e : M ≃ Fin n represents the natural number tupleIndex (e ∘ x) < n ^ k in base n (little-endian).

The relational language v.powerLanguage describes the numbers below n ^ k together with the input tables:

• a binary relation powerLt for the strict linear order < on Fin (n ^ k),
• a unary relation powerIsElem for numbers < n (those whose high k - 1 digits vanish),
• for each symbol i : Fin v.count of arity a = v.arity i, a unary relation powerInTable i for numbers < n ^ a (those whose high k - a digits vanish), and
• for each symbol i : Fin v.count of arity a = v.arity i, a unary relation powerTableBit i holding of m < n ^ a when the m-th bit of the i-th relation table is true.

We construct a first-order interpretation v.powerInterpretation k har of dimension Fin k from L.sum ESO.orderLanguage to v.powerLanguage and prove (v.powerEquiv) that on (M, e) the interpreted structure is isomorphic to (Fin (n ^ k), v.powerStructure (v.encode M e) (n ^ k)). Pulling back along this interpretation via FO.Interpretation.onESOSentence therefore turns an existential second-order sentence about the numeric structure Fin (n ^ k) into one about M (v.realize_onESOSentence_powerInterpretation). Machine simulations in descriptive complexity (Fagin, Immerman–Vardi, Grädel, NL ⊆ FO(TC)) run on this numeric structure.

Main definitions

• Cslib.Logic.Vocabulary.powerLanguage, Cslib.Logic.Vocabulary.powerIsElem, Cslib.Logic.Vocabulary.powerInTable, Cslib.Logic.Vocabulary.powerTableBit, Cslib.Logic.Vocabulary.powerLt: the relational language of the k-th power structure and its symbols.
• Cslib.Logic.Vocabulary.powerStructure: the canonical v.powerLanguage-structure on Fin B induced by an EncodedStructure.
• Cslib.Logic.Vocabulary.powerInterpretation: the first-order interpretation of dimension Fin k from L.sum ESO.orderLanguage to v.powerLanguage.

Main results

• Cslib.Logic.Vocabulary.powerEquiv: the structure interpreted by v.powerInterpretation in (M, orderRelOfEquiv e) is isomorphic to Fin (n ^ k) with v.powerStructure (v.encode M e).
• Cslib.Logic.Vocabulary.realize_onESOSentence_powerInterpretation: pulling an existential second-order sentence back along v.powerInterpretation preserves its truth value.

References

• R. Fagin, Generalized first-order spectra and polynomial-time recognizable sets
• N. Immerman, Descriptive Complexity

The power language and canonical numeric structure

def Cslib.Logic.Vocabulary.powerLanguage {L : FirstOrder.Language} (v : Vocabulary L) : FirstOrder.Language

The relational language of a power structure over a vocabulary v:

• unary relation .inl () (powerIsElem) testing < n,
• unary relation .inr (.inl i) (powerInTable i) testing < n ^ v.arity i,
• unary relation .inr (.inr i) (powerTableBit i) testing the i-th relation table of v, and
• binary relation () (powerLt) for the strict linear order <.

instance Cslib.Logic.Vocabulary.instIsRelationalPowerLanguage {L : FirstOrder.Language} (v : Vocabulary L) : v.powerLanguage.IsRelational

def Cslib.Logic.Vocabulary.powerLt {L : FirstOrder.Language} (v : Vocabulary L) : v.powerLanguage.Relations 2

The binary relation symbol < of v.powerLanguage.

def Cslib.Logic.Vocabulary.powerIsElem {L : FirstOrder.Language} (v : Vocabulary L) : v.powerLanguage.Relations 1

The unary relation symbol < n of v.powerLanguage.

def Cslib.Logic.Vocabulary.powerInTable {L : FirstOrder.Language} (v : Vocabulary L) (i : Fin v.count) : v.powerLanguage.Relations 1

The unary relation symbol < n ^ v.arity i of v.powerLanguage.

def Cslib.Logic.Vocabulary.powerTableBit {L : FirstOrder.Language} (v : Vocabulary L) (i : Fin v.count) : v.powerLanguage.Relations 1

The unary relation symbol for the i-th relation table of v in v.powerLanguage.

@[instance_reducible]

def Cslib.Logic.Vocabulary.powerStructure {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (B : ℕ) : v.powerLanguage.Structure (Fin B)

The canonical v.powerLanguage-structure on Fin B induced by an EncodedStructure a: powerLt is < on Fin B, powerIsElem is < a.1, powerInTable i is < a.1 ^ v.arity i, and powerTableBit i holds of m when m < a.1 ^ v.arity i and bit m of the i-th table of a is true.

theorem Cslib.Logic.Vocabulary.relMap_powerInTable {L : FirstOrder.Language} (v : Vocabulary L) (a : EncodedStructure) (B : ℕ) (i : Fin v.count) (x : Fin 1 → Fin B) : FirstOrder.Language.Structure.RelMap (v.powerInTable i) x ↔ ↑(x 0) < a.1 ^ v.arity i

The first-order interpretation of v.powerLanguage on k-tuples

@[reducible, inline]

abbrev Cslib.Logic.Vocabulary.ltRel {L : FirstOrder.Language} : (L.sum ESO.orderLanguage).Relations 2

The binary relation symbol < of ESO.orderLanguage, inside L.sum ESO.orderLanguage.

def Cslib.Logic.Vocabulary.ltVarFormula {L : FirstOrder.Language} {α : Type u_1} (p q : α) : (L.sum ESO.orderLanguage).Formula α

The formula x < y in L.sum ESO.orderLanguage for free variables p, q : α.

def Cslib.Logic.Vocabulary.isMinVarFormula {L : FirstOrder.Language} {α : Type u_1} (p : α) : (L.sum ESO.orderLanguage).Formula α

The formula ∀ z, ¬ (z < x_p) in L.sum ESO.orderLanguage, saying that x_p is the minimum element of the linear order.

noncomputable def Cslib.Logic.Vocabulary.powerLtFormula {L : FirstOrder.Language} (k : ℕ) : (L.sum ESO.orderLanguage).Formula (Fin 2 × Fin k)

The colexicographic < formula on two k-tuples in L.sum ESO.orderLanguage.

noncomputable def Cslib.Logic.Vocabulary.highZeroFormula {L : FirstOrder.Language} (k a : ℕ) : (L.sum ESO.orderLanguage).Formula (Fin 1 × Fin k)

The formula testing that all coordinates at indices ≥ a are the minimum element.

noncomputable def Cslib.Logic.Vocabulary.powerTableBitFormula {L : FirstOrder.Language} (v : Vocabulary L) (k : ℕ) (har : ∀ (i : Fin v.count), v.arity i ≤ k) (idx : Fin v.count) : (L.sum ESO.orderLanguage).Formula (Fin 1 × Fin k)

The formula defining powerTableBit idx on a k-tuple.

noncomputable def Cslib.Logic.Vocabulary.powerInterpretation {L : FirstOrder.Language} (v : Vocabulary L) (k : ℕ) (har : ∀ (i : Fin v.count), v.arity i ≤ k) : FO.Interpretation (L.sum ESO.orderLanguage) v.powerLanguage (Fin k)

The first-order interpretation of v.powerLanguage in L.sum ESO.orderLanguage of dimension Fin k.

def Cslib.Logic.Vocabulary.powerEquiv {L : FirstOrder.Language} (v : Vocabulary L) (k : ℕ) (hk : 1 ≤ k) (har : ∀ (i : Fin v.count), v.arity i ≤ k) (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) : v.powerLanguage.Equiv ((v.powerInterpretation k har).Model M) (Fin (n ^ k))

The power isomorphism: when M is expanded by the strict linear order of e : M ≃ Fin n, the structure interpreted by v.powerInterpretation k har is isomorphic to Fin (n ^ k) with v.powerStructure (v.encode M e) (n ^ k).

theorem Cslib.Logic.Vocabulary.realize_onESOSentence_powerInterpretation {L : FirstOrder.Language} (v : Vocabulary L) (k : ℕ) (hk : 1 ≤ k) (har : ∀ (i : Fin v.count), v.arity i ≤ k) (M : Type) [L.Structure M] {n : ℕ} (e : M ≃ Fin n) (Ψ : ESO.Sentence v.powerLanguage) : (FO.Interpretation.onESOSentence Ψ).Realize M ↔ Ψ.Realize (Fin (n ^ k))

Pulling back an existential second-order sentence Ψ over v.powerLanguage along v.powerInterpretation k har holds in (M, orderRelOfEquiv e) iff Ψ holds in Fin (n ^ k) with v.powerStructure (v.encode M e) (n ^ k).