The abstract PC-class membership predicate (issue #10, Unit 4) #
PCMem g Θ M — a structure M for the base language L is in the projective class of an
L'-sentence Θ along g : L →ᴸ L' iff M itself (same carrier) expands to an
L'-structure modelling Θ. This is Marker's PC_{ω₁ω} notion (Corollary 4.22): membership
is existence of a same-carrier expansion, enforced here by LHom.IsExpansionOn.
Deliberately language-generic and free of any nonemptiness assumption; the López–Escobar
specialization (baseGraphEmb, code compatibility) lives in Methods/LopezEscobar/PCMem.lean.
def
FirstOrder.Language.PCMem
{L : Language}
{L' : Language}
(g : L →ᴸ L')
(Θ : L'.Sentenceω)
(M : Type u_1)
[L.Structure M]
:
Projective-class membership: M (as an L-structure) expands, on the same carrier, to
an L'-structure satisfying Θ. No nonemptiness is built in.
Equations
- FirstOrder.Language.PCMem g Θ M = ∃ (S' : L'.Structure M), g.IsExpansionOn M ∧ Θ.Realize M