Canonical ordered interpretations on full tuple universes

Only the formulas for the output input relations are supplied by a client. The full domain, canonical order, BIT and numeric constants are constructed from the native tuple formulas. The existing relational interpretation and formula-defined-constant pullback provide the syntax translation. A language map puts the genuine numeric constants into Mathlib's constant extension; no numeric relation table or semantic certificate is an input to the construction. The target input vocabulary is relational; the source vocabulary may contain functions.

For source size at least two and positive tuple dimension, the resulting structure is isomorphic to its canonically ordered rank universe. Arbitrary restricted domains still require explicit numeric definitions and their correctness proofs. No ordered machine or capture theorem is asserted.

Main definitions

• Cslib.Logic.FO.Ordered.FullTupleInterpretation: output input-relation formulas.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.toInterpretation: full relational interpretation.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.onFormula: native constant-aware pullback.

Main results

• Cslib.Logic.FO.Ordered.FullTupleInterpretation.modelEquiv: canonical ordered rank semantics.
• Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onFormula: formula truth preservation.

References

• N. Immerman, Descriptive Complexity, Definition 1.26, Remark 1.32, and Exercise 1.33. Formula pullback uses the existing formalization of Proposition 3.5.

@[reducible, inline]

abbrev Cslib.Logic.FO.Ordered.relationalLanguage (L : FirstOrder.Language) : FirstOrder.Language

The relation symbols of an ordered language, separated from its numeric constants.

instance Cslib.Logic.FO.Ordered.instIsRelationalRelationalLanguage (L : FirstOrder.Language) : (relationalLanguage L).IsRelational

def Cslib.Logic.FO.Ordered.constantsLanguageMap (L : FirstOrder.Language) [L.IsRelational] : language L →ᴸ (relationalLanguage L).withConstants (NumericFunction 0)

View an ordered relational vocabulary as a relational core with genuine numeric constants.

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

A full-tuple ordered interpretation supplies only the definitions of output input relations. Canonical numeric symbols are supplied by the library's native tuple formulas.

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

  The formula defining an output relation on blocks of k source variables.

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

The whole tuple universe, with both input and canonical numeric relation definitions.

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

Reuse the coordinate definitions of zero, one and maximum. Dimension zero has no canonical ordered target and its constant formulas are false.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.constants_valid {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (hk : 0 < k) : I.constants.Valid (Fin n)

The canonical target constants exist uniquely on every positive-dimensional full domain.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.lexRank_constants_value {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (hk : 0 < k) (c : NumericFunction 0) : lexRank ↑(I.constants.value ⋯ c) = c.index (n ^ k)

The selected constants have the exact canonical numerical ranks.

@[instance_reducible]

def Cslib.Logic.FO.Ordered.FullTupleInterpretation.inputStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L'.IsRelational] : L'.Structure (Fin (n ^ k))

The target input relations on the canonical rank universe. Numeric symbols are supplied separately by numericStructure, with no target numeric tables as parameters.

@[instance_reducible]

noncomputable def Cslib.Logic.FO.Ordered.FullTupleInterpretation.modelStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L'.IsRelational] (hk : 0 < k) : (language L').Structure (I.toInterpretation.Model (Fin n))

The actual ordered target structure on interpreted tuples, including numeric constants.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.two_le_pow {k n : ℕ} [Fact (2 ≤ n)] (hk : 0 < k) : 2 ≤ n ^ k

The canonical rank universe also has at least two elements.

def Cslib.Logic.FO.Ordered.FullTupleInterpretation.modelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L'.IsRelational] (hk : 0 < k) : (language L').Equiv (I.toInterpretation.Model (Fin n)) (Fin (n ^ k))

Ranking the interpreted tuples preserves all input relations and canonical numeric symbols, including the genuine target constants zero, one and maximum.

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

Pull back any ordered target formula, using the existing constant-aware interpretation.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L'.IsRelational] {α : Type u_1} (hk : 0 < k) (φ : (language L').Formula α) (v : α → Fin k → Fin n) : ((I.onFormula φ).Realize fun (p : α × Fin k) => v p.1 p.2) ↔ φ.Realize fun (a : α) => lexEquiv (v a)

Native pullback agrees with evaluation on the canonical rank universe, for every assignment.

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

Pull back a sentence over the canonically expanded target language.

theorem Cslib.Logic.FO.Ordered.FullTupleInterpretation.realize_onSentence {L : FirstOrder.Language} {L' : FirstOrder.Language} {k : ℕ} (I : FullTupleInterpretation L L' k) {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] [L'.IsRelational] (hk : 0 < k) (φ : (language L').Sentence) : Fin n ⊨ I.onSentence φ ↔ Fin (n ^ k) ⊨ φ

Sentence truth is preserved on the canonical rank universe.