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.
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 := ⋯ }
Instances For
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.
Instances For
Sentence-level predicates #
Stated ambiently, so that no Polish refinement of the model subtype appears in the definitions.
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.