Documentation

Complexity.Logics.FirstOrder.Ordered.Interpretation

Canonical numeric expansions as sources of first-order interpretations #

The existing FO.Interpretation accepts arbitrary source languages, including the numeric constants, while its interpreted target remains relational. Forgetting the canonical numeric symbols is a one-dimensional interpretation whose interpreted structure is isomorphic to the input. Its pullback therefore preserves every input sentence, including quantified sentences.

No new interpretation syntax is introduced. Target constants and canonical full-tuple numeric preservation are supplied separately in Ordered.FullTuple, using Ordered.TupleBit; numeric-preserving full-tuple composition is in Ordered.FullTuple.Composition. This forgetting bridge does not supply an ordered reduction or machine bound.

Main definitions #

Main results #

References #

source
def Cslib.Logic.FO.Ordered.forget (L : FirstOrder.Language) :
Interpretation (language L) L Unit

Forget the numeric expansion, retaining the whole input universe and its relations.

Instances For
    source
    def Cslib.Logic.FO.Ordered.forgetEquiv {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] :
    L.Equiv ((forget L).Model (Fin n)) (Fin n)

    The relational structure obtained by forgetting the canonical numeric symbols is the input.

    Instances For
      source
      @[simp]
      theorem Cslib.Logic.FO.Ordered.forgetEquiv_apply {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (x : (forget L).Model (Fin n)) :
      forgetEquiv x = ↑x ()
      source
      theorem Cslib.Logic.FO.Ordered.realize_forget_onSentence {L : FirstOrder.Language} [L.IsRelational] {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] (φ : L.Sentence) :
      Fin n ⊨ (forget L).onSentence φ ↔ Fin n ⊨ φ

      Pullback through the existing relational interpretation recovers the input sentence's truth.