Ordered interpretations with a domain formula

An ordered interpretation of dimension k supplies a domain formula and formulas for the target input relations, all over the canonically ordered source language. In a source structure the universe of the image is the set of k-tuples satisfying the domain formula, ordered lexicographically with the first coordinate most significant. Up to the rank isomorphism, this is the image of [Immerman1999, Definition 1.26]: here the domain tuples are renumbered by rank onto Fin m, where m is their number, and the target relations are evaluated at the unranked tuples.

The canonical numerics of the image are those of Fin m; nothing about their definability is assumed at this level. A first-order query on ordered structures must include first-order definitions of the target numerics [Immerman1999, Remark 1.32], and without the assumption that the domain formula is true, target BIT need not be first-order definable in the image [Immerman1999, the paragraph after Exercise 1.33]. These semantic maps are therefore more general than Immerman's first-order queries: his parity example shows that an image whose numerics are not certified need not be a first-order query. The example is cited, not formalized. His numeric definitions are the certificates of Ordered.DomainInterpretation.Certificate, which first-order reductions (Ordered.Reduces) require.

An ordered target structure needs at least two elements [Immerman1999, Proviso 1.15]. An interpretation is admissible when its domain has at least two tuples in every source. This is the library's convention, motivated by that proviso; Immerman's definition does not discuss smaller domains.

Main definitions

• Cslib.Logic.FO.Ordered.DomainInterpretation: a domain formula and target relation formulas.
• Cslib.Logic.FO.Ordered.DomainInterpretation.card: the number of domain tuples.
• Cslib.Logic.FO.Ordered.DomainInterpretation.unrank: the domain tuple of each rank.
• Cslib.Logic.FO.Ordered.DomainInterpretation.rank: the rank of each domain tuple.
• Cslib.Logic.FO.Ordered.DomainInterpretation.inputStructure: the target relations on ranks.
• Cslib.Logic.FO.Ordered.DomainInterpretation.Admissible: at least two domain tuples everywhere.
• Cslib.Logic.FO.Ordered.DomainInterpretation.map: the image of a source structure.
• Cslib.Logic.FO.Ordered.DomainInterpretation.toFOInterpretation: the same formulas as an order-free interpretation.
• Cslib.Logic.FO.Ordered.IsDomainMap: the images of admissible interpretations.

Main results

• Cslib.Logic.FO.Ordered.DomainInterpretation.lexRank_unrank_lt_lexRank_unrank_iff: ranks number domain tuples in lexicographic order.
• Cslib.Logic.FO.Ordered.DomainInterpretation.card_filter_lt_unrank: the rank of a domain tuple counts the domain tuples before it.
• Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_eq_of_strictMono: any increasing enumeration of the domain is unrank.
• Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_of_forall: on the full tuple domain, ranks are lexicographic ranks.
• Cslib.Logic.FO.Ordered.DomainInterpretation.relMap_map: target relations in the image.

References

• N. Immerman, Descriptive Complexity, Proviso 1.15, Definition 1.26, Remark 1.32, Exercise 1.33 and the paragraph after it.

structure Cslib.Logic.FO.Ordered.DomainInterpretation (L : FirstOrder.Language) (L' : FirstOrder.Language) (k : ℕ) : Type (max (max u_1 u_2) u_4)

An ordered interpretation of dimension k of L' in L: a domain formula on k-tuples, and for each relation symbol of L' a formula with a block of k variables per argument. All formulas are over the canonically ordered source language.

• domain : (language L).Formula (Fin k)

  The domain formula: the image consists of the tuples satisfying it.

• rel {r : ℕ} : L'.Relations r → (language L).Formula (Fin r × Fin k)

  The formula defining a target relation on blocks of k source variables.

def Cslib.Logic.FO.Ordered.DomainInterpretation.toFOInterpretation {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) : Interpretation (language L) L' (Fin k)

The same formulas, as an order-free interpretation of L' in the canonically ordered source language, with tuples of Fin k as domain elements.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.domainRanks {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) (M : Structure L) : Finset (Fin (M.size ^ k))

The lexicographic ranks, among all k-tuples, of the domain tuples.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.card {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) (M : Structure L) : ℕ

The number of domain tuples: the size of the image.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) (M : Structure L) (i : Fin (I.card M)) : Fin k → Fin M.size

The domain tuple of a given rank, in lexicographic order.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_eq_card_filter {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} [DecidablePred fun (x : Fin k → Fin M.size) => I.domain.Realize x] : I.card M = {x : Fin k → Fin M.size | I.domain.Realize x}.card

The domain tuples are counted by card.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.realize_domain_unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (i : Fin (I.card M)) : I.domain.Realize (I.unrank M i)

The tuple of every rank satisfies the domain formula.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.lexEquiv_unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (i : Fin (I.card M)) : lexEquiv (I.unrank M i) = ((I.domainRanks M).orderEmbOfFin ⋯) i

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.lexRank_unrank_lt_lexRank_unrank_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} {i j : Fin (I.card M)} : lexRank (I.unrank M i) < lexRank (I.unrank M j) ↔ i < j

Ranks number the domain tuples in lexicographic order.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.strictMono_lexRank_unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} : StrictMono fun (i : Fin (I.card M)) => lexRank (I.unrank M i)

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.lexRank_unrank_le_lexRank_unrank_iff {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} {i j : Fin (I.card M)} : lexRank (I.unrank M i) ≤ lexRank (I.unrank M j) ↔ i ≤ j

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} : Function.Injective (I.unrank M)

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.exists_unrank_eq {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} {x : Fin k → Fin M.size} (hx : I.domain.Realize x) : ∃ (i : Fin (I.card M)), I.unrank M i = x

Every domain tuple has a rank.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.rank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) (M : Structure L) (x : Fin k → Fin M.size) (hx : I.domain.Realize x) : Fin (I.card M)

The rank of a domain tuple.

@[simp]

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_rank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} {x : Fin k → Fin M.size} (hx : I.domain.Realize x) : I.unrank M (I.rank M x hx) = x

@[simp]

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.rank_unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (i : Fin (I.card M)) : I.rank M (I.unrank M i) ⋯ = i

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_filter_lt_unrank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} [DecidablePred fun (x : Fin k → Fin M.size) => I.domain.Realize x] (i : Fin (I.card M)) : {y : Fin k → Fin M.size | I.domain.Realize y ∧ lexRank y < lexRank (I.unrank M i)}.card = ↑i

The rank of a domain tuple counts the domain tuples before it in lexicographic order.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.val_rank {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} [DecidablePred fun (x : Fin k → Fin M.size) => I.domain.Realize x] {x : Fin k → Fin M.size} (hx : I.domain.Realize x) : ↑(I.rank M x hx) = {y : Fin k → Fin M.size | I.domain.Realize y ∧ lexRank y < lexRank x}.card

The rank of a domain tuple, as a count of the domain tuples before it.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_eq_of_strictMono {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} {m : ℕ} (g : Fin m → Fin k → Fin M.size) (hdom : ∀ (i : Fin m), I.domain.Realize (g i)) (hsurj : ∀ (x : Fin k → Fin M.size), I.domain.Realize x → ∃ (i : Fin m), g i = x) (hmono : StrictMono fun (i : Fin m) => lexRank (g i)) : ∃ (h : I.card M = m), ∀ (i : Fin (I.card M)), I.unrank M i = g (Fin.cast h i)

Characterization of ranks. An enumeration of exactly the domain tuples that increases in lexicographic order is unrank, up to the size cast.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.card_of_forall {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (h : ∀ (x : Fin k → Fin M.size), I.domain.Realize x) : I.card M = M.size ^ k

When every tuple is in the domain, there are M.size ^ k of them.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.unrank_of_forall {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (h : ∀ (x : Fin k → Fin M.size), I.domain.Realize x) (i : Fin (I.card M)) : I.unrank M i = lexEquiv.symm (Fin.cast ⋯ i)

When every tuple is in the domain, ranks are lexicographic ranks among all tuples.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.lexRank_unrank_of_forall {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} (h : ∀ (x : Fin k → Fin M.size), I.domain.Realize x) (i : Fin (I.card M)) : lexRank (I.unrank M i) = ↑i

The image

def Cslib.Logic.FO.Ordered.DomainInterpretation.Admissible {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) : Prop

An interpretation is admissible when every source has at least two domain tuples, so that its image carries distinct canonical constants 0 and 1.

@[instance_reducible]

def Cslib.Logic.FO.Ordered.DomainInterpretation.inputStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) (M : Structure L) [L'.IsRelational] : L'.Structure (Fin (I.card M))

The target input relations on the ranks of the domain tuples. Numeric symbols are the canonical ones of Fin (I.card M).

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.map {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : DomainInterpretation L L' k) [L'.IsRelational] (hI : I.Admissible) (M : Structure L) : Structure L'

The image of a source structure under an admissible interpretation.

@[simp]

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.size_map {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} [L'.IsRelational] (hI : I.Admissible) : (I.map hI M).size = I.card M

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.relMap_map {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} {M : Structure L} [L'.IsRelational] (hI : I.Admissible) {r : ℕ} (R : L'.Relations r) (x : Fin r → Fin (I.map hI M).size) : FirstOrder.Language.Structure.RelMap R x ↔ (I.rel R).Realize fun (p : Fin r × Fin k) => I.unrank M (x p.1) p.2

A target relation holds of some ranks when its formula holds of the unranked tuples.

def Cslib.Logic.FO.Ordered.IsDomainMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (f : Structure L → Structure L') : Prop

The maps between ordered structures given by admissible ordered interpretations with a domain formula, with no numeric certificate.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.isDomainMap {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {k : ℕ} {I : DomainInterpretation L L' k} (hI : I.Admissible) : IsDomainMap (I.map hI)

The image of an admissible interpretation is a domain map.