Documentation

CslibFrontier.Logics.FirstOrder.Ordered.FullTuple.DomainInterpretation

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 #

Main results #

References #

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

The lexicographic rank of constantTuple c is c.index (n ^ (k + 1)).

source
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.

Instances For
    source
    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.

    source
    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.

    source
    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'.

    source
    theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.map_congr {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} [L'.IsRelational] {I I' : FullTupleInterpretation L L' k} (hk : 0 < k) (h : ∀ {n : ℕ} [inst : Fact (2 ≤ n)] [inst_1 : L.Structure (Fin n)] {r : ℕ} (R : L'.Relations r) (x : Fin r × Fin k → Fin n), (I.rel R).Realize x ↔ (I'.rel R).Realize x) :
    I.toDomainInterpretation.map ⋯ = I'.toDomainInterpretation.map ⋯

    Two full-tuple interpretations of positive dimension whose relation formulas agree on every canonical ordered structure induce the same image map.

    source
    theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.map_comp {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} [L'.IsRelational] {L'' : FirstOrder.Language} [L''.IsRelational] {l : ℕ} (J : FullTupleInterpretation L' L'' l) (I : FullTupleInterpretation L L' k) (hk : 0 < k) (hl : 0 < l) (M : Structure L) :
    (J.comp I).toDomainInterpretation.map ⋯ M = J.toDomainInterpretation.map ⋯ (I.toDomainInterpretation.map ⋯ M)

    The image of FullTupleInterpretation.comp is the iterated image for positive dimensions.