Documentation

InfinitaryLogic.Methods.LopezEscobar.PCMem

The López–Escobar PC-class interface (issue #10, Unit 4 commit 1) #

The base embedding baseGraphEmb : L →ᴸ graphLanguage (KLang L) (available because L is relational), and the code compatibility theorem tying the abstract PCMem on ℕ to membership in codeReduct '' ModelsOf Θ. This freezes the PC-class interface independently of López–Escobar's tree machinery.

source
def FirstOrder.Language.baseGraphEmb {L : Language} [L.IsRelational] :
L →ᴸ L.KLang.graphLanguage

The base embedding of L into the relationalized graphLanguage (KLang L): functions are vacuous (L is relational), base relations go to their graph-language base image.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.baseGraphEmb_onRelation {L : Language} [L.IsRelational] {n : ℕ} (R : L.Relations n) :
    baseGraphEmb.onRelation R = GraphRelation.base (Sum.inl R)
    source
    theorem FirstOrder.Language.pcMem_iff_mem_codeReduct_image {L : Language} [L.IsRelational] (Θ : L.KLang.graphLanguage.Sentenceω) (c : L.StructureSpace) :
    c ∈ codeReduct '' ModelsOf Θ ↔ PCMem baseGraphEmb Θ ℕ

    Code compatibility: a base code c is a base reduct of a model of Θ iff ℕ (as the L-structure c.toStructure) is in the projective class of Θ along baseGraphEmb.