Canonical constants as interpreted target symbols

The canonical source expansion defines target constants 0, 1 and max by equality to the corresponding source terms. These definitions satisfy the existence/uniqueness requirement for every canonical Fin n structure with n ≥ 2. Thus the native constant-aware pullback applies to all formulas of the input relational vocabulary expanded by these three target constants.

This supplies target constants in the semantic interpretation API. Native full-tuple BIT is constructed separately in Ordered.TupleBit, and numeric-preserving composition in Ordered.FullTuple.Composition and Ordered.DomainInterpretation.Composition. Ordered logspace and machine-capture results remain separate.

Main definitions

• Cslib.Logic.FO.Ordered.constants: canonical definitions of the three target constants.

Main results

• Cslib.Logic.FO.Ordered.constants_valid: the definitions are valid for every n ≥ 2.
• Cslib.Logic.FO.Ordered.constants_value_val: the selected values are the canonical indices.

References

• N. Immerman, Descriptive Complexity, Section 1.2 and Proposition 3.5.

def Cslib.Logic.FO.Ordered.constants (L : FirstOrder.Language) : (forget L).WithConstants (NumericFunction 0)

Define the target constants by equality to the canonical source constants.

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

Every canonical constant defines exactly one tuple in the forgetting interpretation.

theorem Cslib.Logic.FO.Ordered.constants_value_val {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (c : NumericFunction 0) : ↑(↑((constants L).value ⋯ c) ()) = c.index n

The selected target constants have indices zero, one and n - 1, respectively.