Strict-order interpretations of canonical ordered structures

The one-dimensional interpretation retains every input relation and reads strict order from canonical non-strict order. It allows order-based relational formulas to be reused with the canonical ordered vocabulary, including in the full-tuple power interpretation.

Main definitions

• Cslib.Logic.FO.Ordered.strictOrderInterpretation: the relational strict-order interpretation.
• Cslib.Logic.FO.Ordered.strictOrderEquiv: the isomorphism with the canonical input universe.

Main results

• Cslib.Logic.FO.Ordered.realize_strictOrder_onFormula: arbitrary formula truth is preserved.

References

• N. Immerman, Descriptive Complexity, Definition 1.26 and Proposition 3.5.

def Cslib.Logic.FO.Ordered.strictOrderInterpretation (L : FirstOrder.Language) : Interpretation (language L) (L.sum ESO.orderLanguage) Unit

The one-dimensional interpretation retaining the input relations and reading strict order from canonical non-strict order.

def Cslib.Logic.FO.Ordered.strictOrderEquiv {L : FirstOrder.Language} [L.IsRelational] (M : Structure L) : (L.sum ESO.orderLanguage).Equiv ((strictOrderInterpretation L).Model (Fin M.size)) (Fin M.size)

The canonical strict-order structure interpreted above is the original ordered universe.

theorem Cslib.Logic.FO.Ordered.realize_strictOrder_onFormula {L : FirstOrder.Language} [L.IsRelational] (M : Structure L) {α : Type u_1} (φ : (L.sum ESO.orderLanguage).Formula α) (x : α → Fin M.size) : (((strictOrderInterpretation L).onFormula φ).Realize fun (p : α × Unit) => x p.1) ↔ φ.Realize x

Pulling a relational strict-order formula back to the canonical ordered vocabulary preserves its truth for every free-variable assignment.