9
$\begingroup$

Short version: Is there an analogue of the Ash-Knight-Manasse-Slaman/Chisholm theorem for $E$-recursion?


Long version: I'm interested in "$E$-recursive structure theory," but it's not immediately clear to me what exactly that is; my question is an attempt to tease out one aspect of this.

One of the most basic results in classical computable structure theory is the AKMSC theorem, a particular case of which is the following:

Suppose $\mathfrak{A}$ is a countably infinite structure in a finite language, and $U\subseteq\mathfrak{A}$ is an automorphically fixed (=$\mathcal{L}_{\infty,\infty}$-definable) set. Then the following are equivalent:

  • Both $U$ and $\neg U$ are definable in $\mathfrak{A}$ by a computable infinitary $\Sigma_1$ formula (with finitely many parameters).

  • Whenever $\mathfrak{B}$ is a copy of $\mathfrak{A}$ with domain $\omega$, $U^\mathfrak{B}$ is computable relative to (the atomic diagram of) $\mathfrak{B}$.

So we have a connection between relatively intrinsic computability and definability in a certain logic. Carson/Johnson/Knight/Lange/McCoy/Wallbaum lifted this theorem to the setting of $\omega_1$-recursion, and in fact the argument generalizes to all infinite regular cardinals (I suspect that the result holds for singular cardinals as well, but I'm leery of claiming that).

However, I don't immediately see an analogous result for $E$-recursion. Specifically:

Is there a "definability-based" characterization, in terms of already-introduced logic(s), of when an automorphically fixed $U\subseteq\mathfrak{A}$ has the property that for every $\mathfrak{B}\cong\mathfrak{A}$ we have $$U^\mathfrak{B}\le_Etc(\{\mathfrak{B}\}), \overline{x}$$ for some finite tuple $\overline{x}\in tc(\{\mathfrak{B})$?

(Call such a $U$ "relatively intrinsically $E$-recursive on $\mathfrak{A}$.")


Addenda:

  • There is an easy upper bound, at least assuming that $\mathfrak{A}$ has a constructible copy whose cardinality is a regular cardinal in the sense of $L$: for such a $\mathfrak{A}$, if $U$ is relatively intrinsically $E$-recursive on $\mathfrak{A}$ then both $U$ and $\neg U$ are definable in $\mathfrak{A}$ by $\Sigma_1$ formulas in the sense of $\mathcal{L}_{\vert\mathfrak{A}\vert^+,\vert\mathfrak{A}\vert}$. This follows from building a copy of $\mathfrak{A}$ with domain $L_{\vert\mathfrak{A}\vert}$ and applying the CJKLMW lifting of the AKMSC argument. However, the gap between $\alpha$- and $E$-recursion is in general quite large, so this upper bound is probably terrible.

  • If we try to run the usual forcing argument, things break down almost immediately. Conditions should be "simple" partial maps from transitive sets to the structure. In $\kappa$-recursion theory for $\kappa$ infinite and regular (including $\kappa=\omega$), it's enough to just look at $\kappa$-finite maps. Diving into the details what we really want is for the poset of such maps to be appropriately recursive in the structure itself. However, we now run into a major issue: in order to build a sufficiently generic copy of the structure in question in reality (as opposed to some generic extension of the universe) we need these simple maps to "cover" the structure in an appropriate sense, and - while this is trivial for $\kappa$-recursion - there seems to be no reason for this to hold in the $E$-setting, even for reasonably natural structures.

$\endgroup$
4
  • $\begingroup$ So I do not know the answer, but can offer some perspective: in the case of Kleene's S1-S9, there is no "Kleene T predicate" and the recursion theorem is essentially postulated via S9, as S1-S8 only give one primitive recursion (in higher types). Both imply that one cannot talk about S1-S9 computability in weak systems (say higher-order ATR_0 is needed). Is something similar going on with E-recursion? $\endgroup$ Commented Mar 15, 2021 at 18:27
  • $\begingroup$ @SamSanders I'm not sure I quite get what you mean. In E-recursion, the recursion theorem is proved as in classical recursion theory - I think this is analogous to one of Kleene's alternate presentations of his schemes (I know there are a bunch of equivalent formulations kicking around)? But the reverse-math complexity doesn't seem relevant here, as far as I can tell. Incidentally, one could separately ask about an AKMSC theorem for higher type functionals as well; this is something I've also been thinking about recently. $\endgroup$ Commented Mar 15, 2021 at 21:04
  • $\begingroup$ I should have been more specific: if something does not work in S1-S9-recursion theory, then it is (often) because of the reasons I mentioned (no T-predicate and the recursion thm is given via S9, which is one monolithic inductive definition), $\endgroup$ Commented Mar 16, 2021 at 18:26
  • $\begingroup$ @SamSanders I guess I still don't see how that can be used here. $\endgroup$ Commented Mar 16, 2021 at 19:38

0

You must log in to answer this question.