Documentation

Linglib.Core.ModelTheory.LanguageMap

The monadic language on a type of predicate symbols #

This file defines the monadic first-order language on a type Sym of predicate symbols, the relational counterpart of Language.constantsOn, and its structures. Like constantsOn, it is a language constructor rather than a fixed signature, and it sits beside constantsOn in Mathlib/ModelTheory/LanguageMap.lean.

Main definitions #

Implementation notes #

The monadic signature with individual constants is (monadic Pred)[[Const]], mathlib's Language.withConstants. Its structures are withConstantsStructure over monadic.structure and constantsOn.structure, the constant symbol of c is (monadic Pred).con c, and the relation symbol of P is Sum.inl P.

source
def FirstOrder.Language.monadicRel (Sym : Type u) :
ℕ → Type u

The relation symbols of the monadic language on Sym are the elements of Sym at arity one, with no symbols at any other arity.

Equations
Instances For
    source
    def FirstOrder.Language.monadic (Sym : Type u) :
    Language

    The monadic language on Sym has one unary relation symbol for each element of Sym and no other symbols.

    Equations
    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.monadic_Functions (Sym : Type u) (x✝ : ℕ) :
      (monadic Sym).Functions x✝ = Empty
      source
      @[simp]
      theorem FirstOrder.Language.monadic_Relations (Sym : Type u) (a✝ : ℕ) :
      (monadic Sym).Relations a✝ = monadicRel Sym a✝
      source
      instance FirstOrder.Language.instIsRelationalMonadic (Sym : Type u_1) :
      (monadic Sym).IsRelational
      source
      theorem FirstOrder.Language.monadic_relations_one {Sym : Type u} :
      (monadic Sym).Relations 1 = Sym
      source
      instance FirstOrder.Language.isEmpty_relations_monadic_zero {Sym : Type u} :
      IsEmpty ((monadic Sym).Relations 0)
      source
      instance FirstOrder.Language.isEmpty_relations_monadic_succ_succ {Sym : Type u} {n : ℕ} :
      IsEmpty ((monadic Sym).Relations (n + 2))
      source
      @[instance_reducible]
      def FirstOrder.Language.monadic.structure {Sym : Type u} {E : Type u_1} (holds : Sym → E → Prop) :
      (monadic Sym).Structure E

      The monadic Sym-structure on E interpreting each symbol s as the predicate holds s.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem FirstOrder.Language.monadic.structure_relMap {Sym : Type u} {E : Type u_1} (holds : Sym → E → Prop) (s : Sym) (v : Fin 1 → E) :
        Structure.RelMap s v ↔ holds s (v 0)
        source
        @[instance_reducible]
        instance FirstOrder.Language.monadic.structure.decidableRelMap {Sym : Type u} {E : Type u_1} (holds : Sym → E → Prop) [(s : Sym) → (e : E) → Decidable (holds s e)] {n : ℕ} (r : (monadic Sym).Relations n) (v : Fin n → E) :
        Decidable (Structure.RelMap r v)
        Equations