Order and constants on full tuple universes

Finite disjunctions and conjunctions express first-difference lexicographic order without quantifiers. On every canonical base structure Fin n, n ≥ 2, the formulas agree with the arbitrary-base ranks in Ordered.lexEquiv. For positive tuple dimension, coordinate equalities define canonical zero, one and maximum as target constants through the existing constant-aware interpretation API. Their ranks are exactly 0, 1 and n ^ k - 1.

The interpreted universe here consists of all tuples. Successor and BIT lifting are supplied separately in Ordered.TupleSuccessor and Ordered.TupleBit; canonical interpretations and their composition are in Ordered.FullTuple and Ordered.FullTuple.Composition. These results do not infer numeric predicates for arbitrary restricted domains.

Main definitions

• Cslib.Logic.FO.Ordered.tupleLt, Cslib.Logic.FO.Ordered.tupleLe: native tuple-order formulas.
• Cslib.Logic.FO.Ordered.fullTuple: the full tuple domain, with empty relational target language.
• Cslib.Logic.FO.Ordered.tupleConstants: coordinate definitions of the canonical target constants.

Main results

• Cslib.Logic.FO.Ordered.realize_tupleLt, Cslib.Logic.FO.Ordered.realize_tupleLe: rank semantics.
• Cslib.Logic.FO.Ordered.isQF_tupleLt, Cslib.Logic.FO.Ordered.isQF_tupleLe: quantifier-freeness.
• Cslib.Logic.FO.Ordered.tupleConstants_valid: unique selection in the full tuple domain.
• Cslib.Logic.FO.Ordered.lexRank_tupleConstants_value: exact interpreted constant ranks.

References

• N. Immerman, Descriptive Complexity, Remark 1.32 and Exercise 1.33(1). Ordered.TupleBit supplies the full-domain BIT lifting in Exercise 1.33(3).

theorem Cslib.Logic.FO.Ordered.isAtomic_le (L : FirstOrder.Language) {α : Type u_1} (s t : (language L).Term α) : FirstOrder.Language.BoundedFormula.IsAtomic (le L s t)

theorem Cslib.Logic.FO.Ordered.isAtomic_bit (L : FirstOrder.Language) {α : Type u_1} (s i : (language L).Term α) : FirstOrder.Language.BoundedFormula.IsAtomic (bit L s i)

noncomputable def Cslib.Logic.FO.Ordered.tupleLt (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Strict tuple order: one coordinate increases and all earlier coordinates agree.

noncomputable def Cslib.Logic.FO.Ordered.tupleLe (L : FirstOrder.Language) (k : ℕ) : (language L).Formula (Fin 2 × Fin k)

Weak tuple order, expressed without quantifiers by reversing strict order.

theorem Cslib.Logic.FO.Ordered.isQF_tupleLt (L : FirstOrder.Language) (k : ℕ) : FirstOrder.Language.BoundedFormula.IsQF (tupleLt L k)

The lexicographic order formula on tuples is quantifier-free.

theorem Cslib.Logic.FO.Ordered.isQF_tupleLe (L : FirstOrder.Language) (k : ℕ) : FirstOrder.Language.BoundedFormula.IsQF (tupleLe L k)

The lexicographic weak order formula on tuples is quantifier-free.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_tupleLt {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) : (tupleLt L k).Realize v ↔ (lexRank fun (i : Fin k) => v (0, i)) < lexRank fun (i : Fin k) => v (1, i)

The strict-order formula compares the canonical lexicographic ranks.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_tupleLe {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : Fin 2 × Fin k → Fin n) : (tupleLe L k).Realize v ↔ (lexRank fun (i : Fin k) => v (0, i)) ≤ lexRank fun (i : Fin k) => v (1, i)

The weak-order formula compares the canonical lexicographic ranks.

def Cslib.Logic.FO.Ordered.fullTuple (L : FirstOrder.Language) (k : ℕ) : Interpretation (language L) FirstOrder.Language.empty (Fin k)

The whole tuple universe, with no additional target relation symbols.

def Cslib.Logic.FO.Ordered.constantTuple {n k : ℕ} [Fact (2 ≤ n)] (c : NumericFunction 0) : Fin (k + 1) → Fin n

The canonical full-domain tuple corresponding to a numeric constant symbol.

noncomputable def Cslib.Logic.FO.Ordered.tupleConstants (L : FirstOrder.Language) (k : ℕ) : (fullTuple L (k + 1)).WithConstants (NumericFunction 0)

Define each target constant by coordinate equalities to canonical source constants.

theorem Cslib.Logic.FO.Ordered.realize_tupleConstants {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (c : NumericFunction 0) (x : Fin (k + 1) → Fin n) : ((tupleConstants L k).constant c).Realize x ↔ x = constantTuple c

The constant definitions select exactly their explicit canonical coordinate tuples.

theorem Cslib.Logic.FO.Ordered.isQF_tupleConstants (L : FirstOrder.Language) (k : ℕ) (c : NumericFunction 0) : FirstOrder.Language.BoundedFormula.IsQF ((tupleConstants L k).constant c)

The full-domain constant definitions are quantifier-free.

theorem Cslib.Logic.FO.Ordered.tupleConstants_valid {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] : (tupleConstants L k).Valid (Fin n)

Canonical tuple constants exist uniquely for every base n ≥ 2 and positive dimension.

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

The canonical constant tuples have ranks 0, 1 and n ^ (k + 1) - 1.

theorem Cslib.Logic.FO.Ordered.lexRank_tupleConstants_value {L : FirstOrder.Language} {n k : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (c : NumericFunction 0) : lexRank ↑((tupleConstants L k).value ⋯ c) = c.index (n ^ (k + 1))

The interpreted constant values have exactly the canonical numerical ranks.