Documentation

InfinitaryLogic.Methods.LopezEscobar.TaggedGlue

Tagged-expansion gluing (issue #10, Unit 4 commit 2) #

The critical semantic gate: two PCMem witnesses Sl, Sr for the two side sentences may be different graphLanguage (KLang L)-structures on the same base model M. The glued structure uses Sl on the base-and-left symbols and Sr on the right-witness symbols; it agrees with Sl on the left sentence's occurrence set and with Sr on the right's, so realize_congr_symbolsIn transports both satisfactions to the single combined structure.

Endpoint (pcMem_glue): PCMem ψleft M ∧ PCMem ψright M → ∃ S, Realize ψleft M ∧ Realize ψright M, the realizations using S.

source
@[reducible]
def FirstOrder.Language.gluedStructure {L : Language} {M : Type} (Sl Sr : L.KLang.graphLanguage.Structure M) :
L.KLang.graphLanguage.Structure M

The glued structure: Sr on the right-witness symbols, Sl everywhere else.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem FirstOrder.Language.gluedStructure_agree_left {L : Language} [L.IsRelational] {M : Type} (Sl Sr : L.KLang.graphLanguage.Structure M) {p : (n : ℕ) × L.KLang.GraphRelation n} (hp : p ∈ L.KLang.relSym (L.sideFunsSet PCSide.left) (L.baseRels ∪ L.leftRels)) (x : Fin p.fst → M) :
    Structure.RelMap p.snd x ↔ Structure.RelMap p.snd x

    On base-L and left-witness symbols the glue is Sl (definitionally).

    source
    theorem FirstOrder.Language.gluedStructure_agree_right {L : Language} [L.IsRelational] {M : Type} [instL : L.Structure M] (Sl Sr : L.KLang.graphLanguage.Structure M) (hSlExp : baseGraphEmb.IsExpansionOn M) (hSrExp : baseGraphEmb.IsExpansionOn M) {p : (n : ℕ) × L.KLang.GraphRelation n} (hp : p ∈ L.KLang.relSym (L.sideFunsSet PCSide.right) (L.baseRels ∪ L.rightRels)) (x : Fin p.fst → M) :
    Structure.RelMap p.snd x ↔ Structure.RelMap p.snd x

    On base-L and right-witness symbols the glue is Sr — using the shared base for the L-relations (both Sl and Sr expand the same base).

    source
    theorem FirstOrder.Language.pcMem_glue {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {M : Type} [instL : L.Structure M] (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hL : PCMem baseGraphEmb (L.pcSentence PCSide.left T₀) M) (hR : PCMem baseGraphEmb (L.pcSentence PCSide.right T₁) M) :
    ∃ (S : L.KLang.graphLanguage.Structure M), (L.pcSentence PCSide.left T₀).Realize M ∧ (L.pcSentence PCSide.right T₁).Realize M

    The gluing endpoint: two same-base projective-class witnesses glue to a single model of both side sentences.