The ambient isomorphism relation on coded structures

isoSetoid φ lives on the subtype ↥(ModelsOf φ), which means every statement about it is implicitly a statement about a chosen Polish structure on that subtype. For a perfect set that is the wrong place to work: whether a set is perfect should be a fact about the ambient StructureSpace L, not about a refinement chosen to make one particular model class Polish.

So the isomorphism relation is defined once, ambiently, as structureIsoSetoid L, and isoSetoid φ is its pullback along the subtype inclusion — that is its definition, not a theorem about it. The sentence-level predicates below then quantify over perfect subsets of StructureSpace L contained in ModelsOf φ, and the chosen refinement never enters their statements.

def FirstOrder.Language.structureIsoSetoid (L : Language) [L.IsRelational] : Setoid L.StructureSpace

The ambient isomorphism relation: two codes are related iff the structures they decode on ℕ are L-isomorphic. Stated on all of StructureSpace L, with no reference to any sentence.

Equations

• L.structureIsoSetoid = { r := fun (c₁ c₂ : L.StructureSpace) => Nonempty (L.Equiv ℕ ℕ), iseqv := ⋯ }

def FirstOrder.Language.isoSetoid {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Setoid ↑(ModelsOf φ)

The isomorphism equivalence relation on coded ℕ-models of φ: the ambient relation restricted to the models of φ. Two codes are related iff the decoded structures on ℕ are L-isomorphic.

Equations

• FirstOrder.Language.isoSetoid φ = Setoid.comap Subtype.val L.structureIsoSetoid

theorem FirstOrder.Language.isoSetoid_eq_comap {L : Language} [L.IsRelational] (φ : L.Sentenceω) : isoSetoid φ = Setoid.comap Subtype.val L.structureIsoSetoid

isoSetoid φ is the ambient relation pulled back along the subtype inclusion. True by definition; stated so consumers can rewrite with it without unfolding.

theorem FirstOrder.Language.isoSetoid_r_iff {L : Language} [L.IsRelational] {φ : L.Sentenceω} {c₁ c₂ : ↑(ModelsOf φ)} : (isoSetoid φ) c₁ c₂ ↔ L.structureIsoSetoid ↑c₁ ↑c₂

Membership in the pulled-back relation is membership in the ambient one.

Sentence-level predicates

Stated ambiently, so that no Polish refinement of the model subtype appears in the definitions.

def FirstOrder.Language.Sentenceω.HasPerfectSetOfPairwiseNonisomorphicNatModels {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Prop

φ has a perfect set of pairwise non-isomorphic countable models.

Equations

• φ.HasPerfectSetOfPairwiseNonisomorphicNatModels = HasPerfectAntichainOn L.structureIsoSetoid (FirstOrder.Language.ModelsOf φ)

def FirstOrder.Language.Sentenceω.IsThinOnNatModels {L : Language} [L.IsRelational] (φ : L.Sentenceω) : Prop

φ is thin on its countable models: no such perfect set.

Equations

• φ.IsThinOnNatModels = IsThinOn L.structureIsoSetoid (FirstOrder.Language.ModelsOf φ)

theorem FirstOrder.Language.Sentenceω.isThinOnNatModels_iff {L : Language} [L.IsRelational] {φ : L.Sentenceω} : φ.IsThinOnNatModels ↔ ¬φ.HasPerfectSetOfPairwiseNonisomorphicNatModels

theorem FirstOrder.Language.Sentenceω.HasPerfectSetOfPairwiseNonisomorphicNatModels.continuum_le {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (h : φ.HasPerfectSetOfPairwiseNonisomorphicNatModels) : Cardinal.continuum ≤ Cardinal.mk (Quotient (isoSetoid φ))

The bridge to the existing quotient: a perfect set of pairwise non-isomorphic models gives continuum-many isomorphism classes.

The antichain lives in the ambient space, while the quotient is over the subtype, so the transversal is transported through the inclusion — which is exactly what isoSetoid_eq_comap licenses.

From a Polish refinement back to the ambient space

A Cantor antichain is built where the model class is well behaved — in a finer Polish topology of the kind modelsOf_isClopenable supplies. The perfect set, though, must be perfect in the ambient StructureSpace L, or IsThinOnNatModels would be a statement about whichever refinement happened to be chosen.

The two steps are ordered so that the delicate one never arises: coarsening is applied to the Cantor antichain, where only continuity moves, and perfectness is then obtained in the ambient space. Nothing here asserts that perfectness survives coarsening — it does not in general.

theorem FirstOrder.Language.Sentenceω.hasPerfectSet_of_ambient_cantorAntichain {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} (h : HasCantorAntichainOn L.structureIsoSetoid (ModelsOf φ)) : φ.HasPerfectSetOfPairwiseNonisomorphicNatModels

The ambient half of the route: a Cantor antichain on the model class in the ambient topology gives a perfect set of pairwise non-isomorphic models.

StructureSpace L is metrizable but carries no chosen metric, so the T2Space instance that HasCantorAntichainOn.hasPerfectAntichainOn needs is produced here rather than assumed.

theorem FirstOrder.Language.Sentenceω.hasPerfectSet_of_refined_cantorAntichain {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {φ : L.Sentenceω} {t' : TopologicalSpace L.StructureSpace} (hle : t' ≤ FirstOrder.Language.ambientTop✝ L) (h : HasCantorAntichainOn L.structureIsoSetoid (ModelsOf φ)) : φ.HasPerfectSetOfPairwiseNonisomorphicNatModels

A Cantor antichain in any finer topology yields an ambient perfect set of pairwise non-isomorphic models.

theorem FirstOrder.Language.Sentenceω.exists_clopenable_refinement_forcing_perfectSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (φ : L.Sentenceω) : ∃ t' ≤ FirstOrder.Language.ambientTop✝ L, PolishSpace L.StructureSpace ∧ IsClosed (ModelsOf φ) ∧ IsOpen (ModelsOf φ) ∧ (HasCantorAntichainOn L.structureIsoSetoid (ModelsOf φ) → φ.HasPerfectSetOfPairwiseNonisomorphicNatModels)

The refinement modelsOf_isClopenable produces is one the route above accepts, and it is still genuinely clopen: the conclusion keeps IsClosed[t'] and IsOpen[t'] alongside the implication, so a consumer needing the clopen structure — as the tiered counting theorem may — does not have to rebuild the refinement.