Canonical ordered first-order structures

The numeric vocabulary contains ≤, BIT, and the constants 0, 1, and max. On Fin n, with 2 ≤ n, these have their canonical meanings computed from the natural indices. In BIT(x, i), bit zero is the least significant bit. The numeric tables are not additional input. An input language is expanded by Mathlib's Language.sum; its existing functions, constants and relations retain their interpretations. Formulas and terms are Mathlib's existing syntax, so numeric constants can occur directly in relation arguments, equalities and quantified formulas.

This is the canonical-structure prerequisite for ordered descriptive complexity. Native full-tuple BIT and canonical full-tuple interpretations are supplied in Ordered.TupleBit and Ordered.FullTuple; their composition is in Ordered.FullTuple.Composition. Machine and circuit capture theorems require separate developments.

Main definitions

• Cslib.Logic.FO.Ordered.numericLanguage: the numeric symbols.
• Cslib.Logic.FO.Ordered.language: expansion of an input language by the numeric vocabulary.
• Cslib.Logic.FO.Ordered.numericStructure: canonical numeric semantics on Fin n, for n ≥ 2.
• Cslib.Logic.FO.Ordered.zero, Cslib.Logic.FO.Ordered.one, Cslib.Logic.FO.Ordered.max: numeric constant terms in the expanded language.
• Cslib.Logic.FO.Ordered.le, Cslib.Logic.FO.Ordered.bit: numeric atoms on arbitrary terms.

Main results

• Cslib.Logic.FO.Ordered.realize_bit: exact zero-indexed BIT semantics.
• Cslib.Logic.FO.Ordered.realize_zero_ne_one: the numeric constants are distinct.
• Cslib.Logic.FO.Ordered.realize_inputFormula: expansion preserves all input formulas.

References

• N. Immerman, Descriptive Complexity, Section 1.2 and Provisos 1.14–1.15. This minimal vocabulary includes order and BIT; no equivalence with addition/multiplication is asserted.
• Earlier canonical-expansion interfaces in S. Schlesinger, Canonical numerical predicates in Complexitylib informed this native Mathlib formulation.

inductive Cslib.Logic.FO.Ordered.NumericFunction : ℕ → Type

The numeric function symbols are constants only.

• zero : NumericFunction 0

  The least element.

• one : NumericFunction 0

  The element with natural index one.

• max : NumericFunction 0

  The greatest element.

def Cslib.Logic.FO.Ordered.instDecidableEqNumericFunction.decEq {a✝ : ℕ} (x✝ x✝¹ : NumericFunction a✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.instDecidableEqNumericFunction {a✝ : ℕ} : DecidableEq (NumericFunction a✝)

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.instFintypeNumericFunctionOfNatNat : Fintype (NumericFunction 0)

@[reducible, inline]

abbrev Cslib.Logic.FO.Ordered.NumericFunction.index {k : ℕ} (c : NumericFunction k) (m : ℕ) : ℕ

The natural index of a canonical numeric constant in a universe of size m.

theorem Cslib.Logic.FO.Ordered.NumericFunction.index_lt {k m : ℕ} (hm : 2 ≤ m) (c : NumericFunction k) : c.index m < m

inductive Cslib.Logic.FO.Ordered.NumericRelation : ℕ → Type

Canonical order and zero-indexed binary digits.

• le : NumericRelation 2

  Weak natural order.

• bit : NumericRelation 2

  bit x i tests the bit of weight 2^i in x.

def Cslib.Logic.FO.Ordered.instDecidableEqNumericRelation.decEq {a✝ : ℕ} (x✝ x✝¹ : NumericRelation a✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.instDecidableEqNumericRelation {a✝ : ℕ} : DecidableEq (NumericRelation a✝)

@[reducible, inline]

abbrev Cslib.Logic.FO.Ordered.numericLanguage : FirstOrder.Language

The canonical numeric vocabulary, including genuine nullary function symbols.

@[reducible, inline]

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

Preserve input symbols and adjoin the canonical numeric vocabulary.

@[instance_reducible]

def Cslib.Logic.FO.Ordered.numericStructure {n : ℕ} (hn : 2 ≤ n) : numericLanguage.Structure (Fin n)

Canonical numeric semantics; the lower bound makes zero and one distinct elements.

@[instance_reducible]

instance Cslib.Logic.FO.Ordered.instStructureNumericLanguageFinOfFactLeNatOfNat {n : ℕ} [Fact (2 ≤ n)] : numericLanguage.Structure (Fin n)

def Cslib.Logic.FO.Ordered.zero (L : FirstOrder.Language) {α : Type u_1} : (language L).Term α

The numeric zero, as an ordinary Mathlib constant term.

def Cslib.Logic.FO.Ordered.one (L : FirstOrder.Language) {α : Type u_1} : (language L).Term α

The numeric one, as an ordinary Mathlib constant term.

def Cslib.Logic.FO.Ordered.max (L : FirstOrder.Language) {α : Type u_1} : (language L).Term α

The greatest element, as an ordinary Mathlib constant term.

def Cslib.Logic.FO.Ordered.le (L : FirstOrder.Language) {α : Type u_1} (s t : (language L).Term α) : (language L).Formula α

Canonical weak order applied to arbitrary terms, including constants.

def Cslib.Logic.FO.Ordered.bit (L : FirstOrder.Language) {α : Type u_1} (s i : (language L).Term α) : (language L).Formula α

Canonical BIT applied to arbitrary terms; the second argument is the zero-based bit index.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_zero_val {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : α → Fin n) : ↑(FirstOrder.Language.Term.realize v (zero L)) = 0

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_one_val {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : α → Fin n) : ↑(FirstOrder.Language.Term.realize v (one L)) = 1

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_max_val {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : α → Fin n) : ↑(FirstOrder.Language.Term.realize v (max L)) = n - 1

theorem Cslib.Logic.FO.Ordered.realize_zero_ne_one {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (v : α → Fin n) : FirstOrder.Language.Term.realize v (zero L) ≠ FirstOrder.Language.Term.realize v (one L)

The numeric constants are distinct in every canonical expanded structure.

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_le {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (s t : (language L).Term α) (v : α → Fin n) : (le L s t).Realize v ↔ FirstOrder.Language.Term.realize v s ≤ FirstOrder.Language.Term.realize v t

@[simp]

theorem Cslib.Logic.FO.Ordered.realize_bit {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (s i : (language L).Term α) (v : α → Fin n) : (bit L s i).Realize v ↔ (↑(FirstOrder.Language.Term.realize v s)).testBit ↑(FirstOrder.Language.Term.realize v i) = true

bit L s i holds exactly when bit i of s is set, counting from the least significant bit.

theorem Cslib.Logic.FO.Ordered.realize_inputFormula {L : FirstOrder.Language} {α : Type u_1} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (φ : L.Formula α) (v : α → Fin n) : (FirstOrder.Language.LHom.sumInl.onFormula φ).Realize v ↔ φ.Realize v

The language inclusion preserves the truth of every input formula, including constants and quantifiers already present in the input language.