One-jump selection and a pure-equality obstruction for the definition map

Definitions and mathematical statement

Question $7$ asks for the complexity of $\varphi\mapsto d_p\varphi$, possibly uniformly in $p$. The source excerpt does not define the ambient theory, coding or output equivalence. The aid's precise interpretation assumes a countable model $M$ in an effectively coded language and a complete type $p(x)$ over $M$ for which the required definitions exist, as in a stable theory. For $\varphi(x;y)$, an output is an actual formula code $\psi(y)$ with parameters from $M$ such that \[ M\models\psi(b)\quad\Longleftrightarrow\quad \varphi(x;b)\in p \qquad(b\in M^{|y|}). \] The definition need not be syntactically unique.

Code $p$ by its characteristic function, supply the elementary diagram of $M$, and put $B=p\oplus\operatorname{ElDiag}(M)$. The aid proves that valid output codes form a nonempty $\Pi^0_1(B)$ subset of ${\mathbb{N}}$: validity is the universal condition over tuples $b$, each instance decidable in $B$. Hence its least code is uniformly computable from the Turing jump $B'$. The procedure also has a $B$-computable approximation with finitely many changes, by choosing the least code not yet refuted. Nonemptiness and the finitely many codes below the true least code ensure eventual stabilization; no computable uniform change bound is asserted.

The uniform computable bound cannot replace that jump in general. Already in an infinite pure-equality model, with $\varphi(x;y)$ equal to $x=y$, the aid constructs a uniformly computable family of complete type oracles. A type is a new-element type if a machine never halts, and a principal type at a sufficiently late named element if it halts. Any uniform syntactic-definition selector distinguishes empty from singleton traces; emptiness of a pure-equality formula is decidable. It would therefore decide the halting set. This is a worst-case uniform lower bound over $p$, not a statement that each fixed type individually needs a jump.

The semantic trace $b\mapsto[\varphi(x;b)\in p]$ is directly $p$-computable from its characteristic coding. Its computation is different from selecting a finite defining formula. If the source intended semantic traces, different type coding, unavailable elementary diagrams, or nondefinable types, the stated selector theorem would not be that same problem.

Short English statement

For definable types with characteristic-function coding and the model's elementary diagram, selecting an actual definition formula has a one-jump upper bound and finite-change approximation. A pure-equality family rules out a computable selector uniform in the type. Semantic traces are easier and are not the same output problem.

Sources

• Local UnsolvedMath registry, permanent ID $20002309$, source code catalogue entry; canonical collection aim-logic-notes.json, notes[84].
• AIM workshop "Computable stability theory," Question $7$: https://aimath.org/pastworkshops/computestabproblems.pdf. The extracted "$\varphi\ 7\to d_p\varphi$" denotes the formula-to-definition map. The record supplies no additional context or attribution. No PDF was opened in this session.
• Supplied research attempt $1$, partial_result, run status "unknown," rigor label "proved," novelty confidence "low." Registry status partially_solved, classification PARTIAL-PROGRESS, updated 14 August 2026. No full authoritative reference for the selector theorem or lower-bound family is supplied; original remarks and literature are empty, with no proposer or year.