Documentation

Complexity.Logics.FirstOrder.Interpretation.Tuple

Interpretations on all tuples #

The relation formulas of an interpretation I of dimension ι define relations on all tuples ι → M of an L-structure M (Interpretation.tupleStructure). When the domain formula holds of every tuple, the interpreted structure is isomorphic to this structure (Interpretation.tupleModelEquiv), so that statements about the interpreted structure become statements about tuples of elements of M, without the subtypes of Interpretation.Model. This generalizes Interpretation.unitStructure from dimension one, where the tuples are identified with the elements themselves, to every dimension.

Through this isomorphism the pullback of a formula along such an interpretation is realized as the formula itself in the structure on tuples (Interpretation.realize_onFormula_tupleStructure). In particular, the domain and relation formulas of a composite J.comp I whose first interpretation I has such a domain are realized as those of J in the structure defined by I on tuples (Interpretation.realize_comp_domain_tupleStructure, Interpretation.realize_comp_rel_tupleStructure), at arbitrary valuations.

Main definitions #

Main results #

References #

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

The relations defined by an interpretation on all tuples ι → M: a relation symbol holds of some tuples when its defining formula holds of their coordinates.

Instances For
    source
    theorem Cslib.Logic.FO.Interpretation.relMap_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) {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 × ι) => x p.1 p.2

    On all tuples, a target relation holds exactly when its defining formula does.

    source
    def Cslib.Logic.FO.Interpretation.tupleModelEquiv {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) (M : Type w) [L.Structure M] (hdom : ∀ (x : ι → M), I.domain.Realize x) :
    L'.Equiv (I.Model M) (ι → M)

    When the domain formula of an interpretation holds of every tuple, the interpreted structure is isomorphic to the tuples with the relations defined by the interpretation.

    Instances For
      source
      @[simp]
      theorem Cslib.Logic.FO.Interpretation.tupleModelEquiv_apply {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) (M : Type w) [L.Structure M] (hdom : ∀ (x : ι → M), I.domain.Realize x) (x : I.Model M) :
      (I.tupleModelEquiv M hdom) x = ↑x
      source
      theorem Cslib.Logic.FO.Interpretation.fun_unit_eq_iff {α : Type u_2} {f g : Unit → α} :
      f = g ↔ f () = g ()

      Equality of functions on Unit is equality at ().

      source
      theorem Cslib.Logic.FO.Interpretation.realize_onFormula_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) {M : Type w} [L.Structure M] [Finite ι] (hdom : ∀ (x : ι → M), I.domain.Realize x) {α : Type u_2} (φ : L'.Formula α) (v : α → ι → M) :
      ((I.onFormula φ).Realize fun (p : α × ι) => v p.1 p.2) ↔ φ.Realize v

      The pullback of a formula along an interpretation whose domain formula holds of every tuple is realized as the formula in the structure defined on tuples.

      source
      theorem Cslib.Logic.FO.Interpretation.realize_comp_domain_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) {M : Type w} [L.Structure M] [Finite ι] {L'' : FirstOrder.Language} {κ : Type u_2} [Finite κ] (J : Interpretation L' L'' κ) (hdom : ∀ (x : ι → M), I.domain.Realize x) (v : κ × ι → M) :
      (J.comp I).domain.Realize v ↔ J.domain.Realize fun (j : κ) (i : ι) => v (j, i)

      The domain formula of a composite J.comp I, when the domain formula of I holds of every tuple, is realized as the domain formula of J in the structure defined by I on tuples.

      source
      theorem Cslib.Logic.FO.Interpretation.realize_comp_rel_tupleStructure {L : FirstOrder.Language} {L' : FirstOrder.Language} [L'.IsRelational] {ι : Type u_1} (I : Interpretation L L' ι) {M : Type w} [L.Structure M] [Finite ι] {L'' : FirstOrder.Language} {κ : Type u_2} [Finite κ] (J : Interpretation L' L'' κ) (hdom : ∀ (x : ι → M), I.domain.Realize x) {n : ℕ} (R : L''.Relations n) (v : Fin n × κ × ι → M) :
      ((J.comp I).rel R).Realize v ↔ (J.rel R).Realize fun (p : Fin n × κ) (i : ι) => v (p.1, p.2, i)

      A relation formula of a composite J.comp I, when the domain formula of I holds of every tuple, is realized as the relation formula of J in the structure defined by I on tuples.