Numbering the elements of an interpreted structure

A first-order interpretation I of dimension ι interprets, in a structure on Fin n, a structure whose elements are the tuples ι → Fin n satisfying the domain formula. Fixing an enumeration e : ι ≃ Fin d of the coordinates, a tuple has an index below n ^ d (Cslib.Logic.tupleIndex), and the elements of the interpreted structure are numbered by the rank of their index among the indices of the domain (Cslib.Logic.FO.Interpretation.rankEquiv): the number of indices of the domain below it. This is the numbering an algorithm computes by counting, as a logarithmic-space transducer for the interpretation does.

Main definitions

• Cslib.Logic.FO.Interpretation.InDomain: the indices of the tuples of the domain.
• Cslib.Logic.FO.Interpretation.domainRank: the number of indices of the domain below a number.
• Cslib.Logic.FO.Interpretation.rankEquiv: the numbering of the interpreted structure by ranks.

Main results

• Cslib.Logic.FO.Interpretation.domainRank_succ: ranks count the indices of the domain.
• Cslib.Logic.FO.Interpretation.rankEquiv_symm_val: the element of a given rank is the tuple whose index has that rank.

References

• N. Immerman, Descriptive Complexity

def Cslib.Logic.FO.Interpretation.InDomain {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} (I : Interpretation L L' ι) (e : ι ≃ Fin d) (n : ℕ) [L.Structure (Fin n)] (u : ℕ) : Prop

The number u is the index of a tuple of the domain of I.

noncomputable def Cslib.Logic.FO.Interpretation.domainRank {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} (I : Interpretation L L' ι) (e : ι ≃ Fin d) (n : ℕ) [L.Structure (Fin n)] (u : ℕ) : ℕ

The number of indices of tuples of the domain below u.

theorem Cslib.Logic.FO.Interpretation.domainRank_zero {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] : I.domainRank e n 0 = 0

theorem Cslib.Logic.FO.Interpretation.domainRank_succ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] (u : ℕ) [Decidable (I.InDomain e n u)] : I.domainRank e n (u + 1) = I.domainRank e n u + if I.InDomain e n u then 1 else 0

Ranks count the indices of the domain: the rank of u + 1 is that of u, plus one when u indexes a tuple of the domain.

theorem Cslib.Logic.FO.Interpretation.domainRank_mono {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] {u u' : ℕ} (h : u ≤ u') : I.domainRank e n u ≤ I.domainRank e n u'

theorem Cslib.Logic.FO.Interpretation.domainRank_lt_of_inDomain {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] {u u' : ℕ} (hu : I.InDomain e n u) (h : u < u') : I.domainRank e n u < I.domainRank e n u'

theorem Cslib.Logic.FO.Interpretation.inDomain_tupleEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] (x : I.Model (Fin n)) : I.InDomain e n ↑((tupleEquiv e) ↑x)

noncomputable def Cslib.Logic.FO.Interpretation.modelCard {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} (I : Interpretation L L' ι) (e : ι ≃ Fin d) (n : ℕ) [L.Structure (Fin n)] : ℕ

The number of elements of the interpreted structure: the number of indices of the domain.

theorem Cslib.Logic.FO.Interpretation.modelCard_le_pow {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] : I.modelCard e n ≤ n ^ d

noncomputable def Cslib.Logic.FO.Interpretation.rankOf {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] (x : I.Model (Fin n)) : Fin (I.modelCard e n)

The rank of the index of an element of the interpreted structure.

theorem Cslib.Logic.FO.Interpretation.rankOf_injective {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] : Function.Injective rankOf

theorem Cslib.Logic.FO.Interpretation.exists_inDomain_of_lt {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] {r : ℕ} (hr : r < I.modelCard e n) : ∃ (u : ℕ), I.InDomain e n u ∧ I.domainRank e n u = r

Every rank below the number of elements is the rank of an index of the domain.

theorem Cslib.Logic.FO.Interpretation.rankOf_surjective {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] : Function.Surjective rankOf

noncomputable def Cslib.Logic.FO.Interpretation.rankEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} (I : Interpretation L L' ι) (e : ι ≃ Fin d) (n : ℕ) [L.Structure (Fin n)] : I.Model (Fin n) ≃ Fin (I.modelCard e n)

The numbering of the interpreted structure by ranks: an element is numbered by the number of indices of the domain below its index.

@[simp]

theorem Cslib.Logic.FO.Interpretation.rankEquiv_apply_val {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] (x : I.Model (Fin n)) : ↑((I.rankEquiv e n) x) = I.domainRank e n ↑((tupleEquiv e) ↑x)

theorem Cslib.Logic.FO.Interpretation.rankEquiv_symm_val {L : FirstOrder.Language} {L' : FirstOrder.Language} {ι : Type u_1} {d : ℕ} {I : Interpretation L L' ι} {e : ι ≃ Fin d} {n : ℕ} [L.Structure (Fin n)] {r : Fin (I.modelCard e n)} {u : ℕ} (hu : I.InDomain e n u) (hr : I.domainRank e n u = ↑r) : (I.rankEquiv e n).symm r = ⟨(tupleEquiv e).symm ⟨u, ⋯⟩, ⋯⟩

The element of a given rank is the tuple whose index is in the domain and has that rank.