Documentation

Complexity.Logics.FirstOrder.Interpretation.Unit

One-dimensional interpretations #

An interpretation of dimension Unit defines its relations on single elements. Its relation formulas define new relations on the universe of the structure itself (Interpretation.unitStructure), and when its domain formula holds of every element, the interpreted structure is isomorphic to this structure (Interpretation.unitModelEquiv). Many first-order reductions, such as complementing a relation, are of this kind; through this isomorphism their correctness is a statement about the input universe, without the tuples and subtypes of Interpretation.Model.

Main definitions #

Main results #

References #

source
@[instance_reducible]
def Cslib.Logic.FO.Interpretation.unitStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (I : Interpretation L L' Unit) (M : Type w) [L.Structure M] :
L'.Structure M

The relations defined by a one-dimensional interpretation on the universe of M itself: a relation symbol holds of some elements when its defining formula holds of them.

Instances For
    source
    theorem Cslib.Logic.FO.Interpretation.relMap_unitStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (I : Interpretation L L' Unit) {M : Type w} [L.Structure M] {n : ℕ} (R : L'.Relations n) (x : Fin n → M) :
    FirstOrder.Language.Structure.RelMap R x ↔ (I.rel R).Realize fun (p : Fin n × Unit) => x p.1

    On single elements, a target relation holds exactly when its defining formula does.

    source
    def Cslib.Logic.FO.Interpretation.unitModelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (I : Interpretation L L' Unit) (M : Type w) [L.Structure M] (hdom : ∀ (x : M), I.domain.Realize fun (x_1 : Unit) => x) :
    L'.Equiv (I.Model M) M

    When the domain formula of a one-dimensional interpretation holds of every element, the interpreted structure is isomorphic to M with the relations defined by the interpretation.

    Instances For
      source
      @[simp]
      theorem Cslib.Logic.FO.Interpretation.unitModelEquiv_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] (I : Interpretation L L' Unit) (M : Type w) [L.Structure M] (hdom : ∀ (x : M), I.domain.Realize fun (x_1 : Unit) => x) (x : I.Model M) :
      (I.unitModelEquiv M hdom) x = ↑x ()