López-Escobar, the easy direction

For arbitrary relational vocabularies the model class of an L_ω₁ω-sentence is PRODUCT-MEASURABLE and ISOMORPHISM-INVARIANT (modelsOf_measurable_invariant); for countable relational vocabularies — where the repository's BorelSpace/StandardBorelSpace (StructureSpace L) instances apply — this is an invariant BOREL subset of the standard Borel structure space (lopezEscobar_easy, the literature statement).

Invariance is the named isomorphism-closed predicate IsomorphismInvariant (an L-isomorphism of the decoded structures transports membership) — equivalent to invariance under the logic action (actionInvariant_iff_isomorphismInvariant, Descriptive/LogicAction.lean).

The hard converse — every isomorphism-invariant Borel class is L_ω₁ω-definable, by Marker's route through Craig interpolation and PC-separation — is proved: lopez_escobar (Methods/LopezEscobar/Separation.lean), packaged with this direction as lopezEscobar_iff in Descriptive/LopezEscobar.lean.

def FirstOrder.Language.IsomorphismInvariant {L : Language} [L.IsRelational] (B : Set L.StructureSpace) : Prop

Isomorphism invariance of a class of coded structures, in isomorphism-closed form: an L-isomorphism of the decoded structures transports membership.

Equations

• FirstOrder.Language.IsomorphismInvariant B = ∀ (c d : L.StructureSpace), Nonempty (L.Equiv ℕ ℕ) → (c ∈ B ↔ d ∈ B)

theorem FirstOrder.Language.lopezEscobar_easy {L : Language} [L.IsRelational] (φ : L.Sentenceω) : MeasurableSet (ModelsOf φ) ∧ IsomorphismInvariant (ModelsOf φ)

López-Escobar, easy direction: every L_ω₁ω-sentence defines a product-measurable, isomorphism-invariant class of coded countable structures. For countable relational vocabularies, this is a Borel class for the Polish topology. The converse is lopez_escobar; the two directions are packaged as lopezEscobar_iff.