Full-tuple interpretations as interpretations with a domain formula

A full-tuple interpretation is the ordered interpretation whose domain formula is true, the usual case of [Immerman1999, Definition 1.26]. Its ranks are the lexicographic ranks of all tuples, so its image and its encoded map agree with the existing full-tuple semantics. For positive dimension it is admissible, and the native tuple formulas for order, BIT and constants [Immerman1999, Exercise 1.33] form its numeric certificate. Full-tuple interpretations of positive dimension therefore give first-order reductions.

Main definitions

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.certificate: the native numeric certificate for FullTupleInterpretation.toDomainInterpretation (defined in Complexity/Logics/FirstOrder/Ordered/FullTuple/Encoding.lean).

Main results

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.relMap_map_toDomainInterpretation: agreement with FullTupleInterpretation.inputStructure.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.isFirstOrderMap_map_toDomainInterpretation: full-tuple images are first-order maps.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.reduces: full-tuple interpretations of positive dimension give first-order reductions.

References

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

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.lexRank_constantTuple {k n : ℕ} [Fact (2 ≤ n)] (c : NumericFunction 0) : lexRank (constantTuple c) = c.index (n ^ (k + 1))

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.certificate {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) (hk : 0 < k) : I.toDomainInterpretation.Certificate

The native tuple formulas for order, BIT and constants certify a positive-dimensional full-tuple interpretation.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.relMap_map_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} {M : Structure L} [L'.IsRelational] (hk : 0 < k) {r : ℕ} (R : L'.Relations r) (x : Fin r → Fin (I.toDomainInterpretation.map ⋯ M).size) : FirstOrder.Language.Structure.RelMap R x ↔ FirstOrder.Language.Structure.RelMap R (Fin.cast ⋯ ∘ x)

The image of a full-tuple interpretation is its canonical rank structure, up to the size cast.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.isFirstOrderMap_map_toDomainInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} [L'.IsRelational] (hk : 0 < k) : IsFirstOrderMap (I.toDomainInterpretation.map ⋯)

Full-tuple images of positive dimension are first-order maps.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.reduces {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : FullTupleInterpretation L L' k} [L'.IsRelational] (hk : 0 < k) {K : Query L} {K' : Query L'} (h : ∀ (M : Structure L), M ∈ K ↔ I.toDomainInterpretation.map ⋯ M ∈ K') : Reduces K K'

Full-tuple interpretations give first-order reductions. A full-tuple interpretation of positive dimension that maps exactly the members of K into K' reduces K to K'.