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.modelsOf_mem_iff_of_equiv {L : Language} [L.IsRelational] (φ : L.Sentenceω) {c d : L.StructureSpace} (e : L.Equiv ℕ ℕ) : c ∈ ModelsOf φ ↔ d ∈ ModelsOf φ

Membership in a sentence's model class is isomorphism-invariant: an L-isomorphism of the decoded structures transports satisfaction.

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

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

The general form (arbitrary relational vocabularies): the model class of a sentence is product-measurable and isomorphism-invariant.

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

López-Escobar, easy direction (countable relational vocabularies): every L_ω₁ω-sentence defines an isomorphism-invariant BOREL class of coded countable structures — here MeasurableSet is Borel for the Polish topology, by the BorelSpace (StructureSpace L) instance, which is what the countable-relations hypothesis activates. (The converse — invariant Borel classes are L_ω₁ω-definable — is lopez_escobar; the two directions are packaged as lopezEscobar_iff.)