Numeric certificates for ordered interpretations

A first-order query on ordered structures must include first-order definitions of the numeric relations and constants of its image [Immerman1999, Remark 1.32]. Without the assumption that the domain formula is true, these need not exist: target BIT need not be first-order definable [Immerman1999, the paragraph after Exercise 1.33]. A numeric certificate for an ordered interpretation supplies these definitions over the source language, on domain tuples, together with a proof that on every source they define the canonical order, BIT and constants 0, 1, max of the rank numbering. The constants are thus the least, second and greatest domain tuples in lexicographic order, as in [Immerman1999, Definition 1.26 and Exercise 1.33(1)].

A certificate turns the interpretation into an order-free interpretation of the ordered target language with formula-defined constants, whose interpreted structure is isomorphic, by ranking, to the image. Hence every ordered target formula pulls back to a source formula with the same truth value [Immerman1999, Proposition 3.5].

Main definitions

• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate: numeric definitions and their correctness on every source.
• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.toInterpretation: the relational interpretation of the ordered target language.
• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.onFormula, Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.onSentence: pullback of ordered target formulas.

Main results

• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.modelEquiv: ranking is an isomorphism of ordered structures onto the image.
• Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.realize_onFormula, Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.realize_onSentence: truth preservation.

References

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

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

A numeric certificate for an ordered interpretation: source formulas defining, on domain tuples, the canonical order, BIT and numeric constants of the rank numbering, with a proof that they do so on every source.

• le : (language L).Formula (Fin 2 × Fin k)

  The definition of the target order on two blocks of k variables.

• bit : (language L).Formula (Fin 2 × Fin k)

  The definition of target BIT on two blocks of k variables.

• const : NumericFunction 0 → (language L).Formula (Fin k)

  The definition of each target constant; domain membership is imposed separately.

• realize_le (M : Structure L) (v : Fin 2 → Fin (I.card M)) : (self.le.Realize fun (p : Fin 2 × Fin k) => I.unrank M (v p.1) p.2) ↔ v 0 ≤ v 1

  The order formula compares ranks.

• realize_bit (M : Structure L) (v : Fin 2 → Fin (I.card M)) : (self.bit.Realize fun (p : Fin 2 × Fin k) => I.unrank M (v p.1) p.2) ↔ (↑(v 0)).testBit ↑(v 1) = true

  The BIT formula is BIT of ranks.

• realize_const (M : Structure L) (c : NumericFunction 0) (i : Fin (I.card M)) : (self.const c).Realize (I.unrank M i) ↔ ↑i = c.index (I.card M)

  The constant formulas select the domain tuples of ranks 0, 1 and card - 1.

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

The relational interpretation of the ordered target language: the domain and relations of I, with the certificate's order and BIT.

def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.constants {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) : C.toInterpretation.WithConstants (NumericFunction 0)

The certificate's definitions of the target constants.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.constants_valid {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} (hI : I.Admissible) : C.constants.Valid (Fin M.size)

Each certificate constant selects the domain tuple of its rank.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.val_rank_value {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} (hI : I.Admissible) (c : NumericFunction 0) : ↑(I.rank M ↑(C.constants.value ⋯ c) ⋯) = c.index (I.card M)

@[instance_reducible]

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.modelStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} [L'.IsRelational] (hI : I.Admissible) : (language L').Structure (C.toInterpretation.Model (Fin M.size))

The interpreted ordered structure, with the certificate's constants.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.modelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} [L'.IsRelational] (hI : I.Admissible) : (language L').Equiv (C.toInterpretation.Model (Fin M.size)) (Fin (I.map hI M).size)

Ranking is an isomorphism from the interpreted ordered structure onto the image, including the canonical order, BIT and constants.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.modelEquiv_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} [L'.IsRelational] (hI : I.Admissible) (x : C.toInterpretation.Model (Fin M.size)) : (C.modelEquiv hI) x = I.rank M ↑x ⋯

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) [L'.IsRelational] {α : Type u_1} (φ : (language L').Formula α) : (language L).Formula (α × Fin k)

Pull back an ordered target formula along a certified interpretation.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} [L'.IsRelational] {α : Type u_1} (hI : I.Admissible) (φ : (language L').Formula α) (v : α → Fin (I.map hI M).size) : ((C.onFormula φ).Realize fun (p : α × Fin k) => I.unrank M (v p.1) p.2) ↔ φ.Realize v

Pullback preserves truth: the pullback holds of the domain tuples of some ranks exactly when the formula holds of these ranks in the image.

noncomputable def Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) [L'.IsRelational] (φ : (language L').Sentence) : (language L).Sentence

Pull back an ordered target sentence along a certified interpretation.

theorem Cslib.Logic.FO.Ordered.DomainInterpretation.Certificate.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} {I : DomainInterpretation L L' k} (C : I.Certificate) {M : Structure L} [L'.IsRelational] (hI : I.Admissible) (φ : (language L').Sentence) : Fin M.size ⊨ C.onSentence φ ↔ Fin (I.map hI M).size ⊨ φ

Pullback preserves sentence truth in the image.