Canonical ordered power structures

The existing power interpretation exposes input truth tables on a polynomially enlarged universe. This module adapts it to the canonical full-tuple interface, so that target order, BIT and numeric constants are defined by the existing tuple formulas. Reversing each tuple block reconciles the power interpretation's little-endian indexing with lexicographic ranking.

Main definitions

• Cslib.Logic.Vocabulary.orderedPowerInterpretation: the full-tuple power interpretation.

Main results

• Cslib.Logic.Vocabulary.realize_orderedPower_rel: exact numerical semantics of input relations.
• Cslib.Logic.Vocabulary.inputStructure_orderedPowerInterpretation: the interpreted input structure is the existing powerStructure, with no supplied numeric tables.

References

• N. Immerman, Descriptive Complexity, Remark 1.32 and Exercise 1.33.

noncomputable def Cslib.Logic.Vocabulary.orderedPowerInterpretation {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (k : ℕ) (har : ∀ (i : Fin v.count), v.arity i ≤ k) : FO.Ordered.FullTupleInterpretation L v.powerLanguage k

Retain the original power-structure input predicates while using canonical lexicographic tuple ranks. All target numeric predicates are supplied by the full-tuple interpretation.

theorem Cslib.Logic.Vocabulary.realize_orderedPower_rel {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (k : ℕ) (har : ∀ (i : Fin v.count), v.arity i ≤ k) (hk : 1 ≤ k) (M : FO.Ordered.Structure L) {r : ℕ} (R : v.powerLanguage.Relations r) (x : Fin r → Fin k → Fin M.size) : (((v.orderedPowerInterpretation k har).rel R).Realize fun (p : Fin r × Fin k) => x p.1 p.2) ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin r) => FO.Ordered.lexEquiv (x i)

The original power predicates evaluated on lexicographically ranked tuples.

theorem Cslib.Logic.Vocabulary.inputStructure_orderedPowerInterpretation {L : FirstOrder.Language} [L.IsRelational] (v : Vocabulary L) (k : ℕ) (har : ∀ (i : Fin v.count), v.arity i ≤ k) (hk : 1 ≤ k) (M : FO.Ordered.Structure L) : (v.orderedPowerInterpretation k har).inputStructure = v.powerStructure (FO.Ordered.encode v M) (M.size ^ k)

The input relations of the full-tuple interpretation agree exactly with the canonical power structure of the native input encoding.