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.
@[reducible]
def
FirstOrder.Language.gluedStructure
{L : Language}
{M : Type}
(Sl Sr : 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
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.