17
$\begingroup$

Let $\mathbf{A}$ be an admissible set (possibly with urelements). I am wondering if there is some good notion of "primitive recursive arithmetic" relative to $\mathbf{A}$. More precisely, I would like to single out a class of $\Pi_{2}$-sentences (with parameters) about $\mathbf{A}$ which reduces to the class of $\Pi_{2}$-theorems of PRA when specialized to the case where $\mathbf{A}$ is the set of hereditarily finite sets. In particular, I would like to single out a special class of "provably total" $\Sigma_1$-definable functions on $\mathbf{A}$, which reduces to the class of primitive recursive functions when $\mathbf{A} =$ hereditarily finite sets.

I would be grateful for any pointers to relevant literature. If it helps, I am primarily interested in the case where $\mathbf{A}$ is the smallest admissible set containing some mathematical structure $M$ (that is, $\mathbf{A} = HYP_M$, in the notation of Barwise's book).

$\endgroup$
  • 1
    $\begingroup$ Moschovakis' book "Elementary induction on abstract structures" develops recursion theory on admissible sets. In the book he proves the Barwise Gandy Moschovakis theorem which says that if $A$ is a transitive set closed under pairing then the inductive relations on the structure $(A,\epsilon)$ are exactly the relations on $A$ which are $\Sigma_1$ over an admissible set. I don't know if this is directly relevant to your question, or if the theory reduces to PRA on $A$ if $A=H_{\omega}$. (see chapter 9 of the book). $\endgroup$ – 16278263789 Jan 21 '15 at 5:36
  • $\begingroup$ When I read this I am reminded of Fenstad and Abstract Recursion Theory. I don't quite know why; it may not fit in with your program. $\endgroup$ – The Masked Avenger Jan 21 '15 at 6:54
  • 5
    $\begingroup$ Jensen and Karp's primitive recursive set functions give your generalized functions, and Michael Rathjen, A proof-theoretic characterization of the primitive recursive set functions, JSL 57(3), 1992 (www1.maths.leeds.ac.uk/~rathjen/PrimRec.pdf) seems to give the theory that you want. $\endgroup$ – Ulrik Buchholtz Jan 21 '15 at 14:43
  • $\begingroup$ @Carlo It is relevant, but I am asking for something more refined: I want to consider not just which sets are $\Sigma_1$-definable in $A$, but when $A$ "knows" that one $\Sigma_1$-set is contained in another. $\endgroup$ – Jacob Lurie Jan 28 '15 at 18:42
  • 1
    $\begingroup$ @Ulrik That paper looks quite relevant, but not exactly what I'm looking for. If I'm reading it right, it seems to be about functions whose totality is provable using very weak set-theoretic assumptions, analogous to the characterization of primitive recursive functions as those functions which are provably total using very weak arithmetic assumptions. But I'm hoping for something which is specific to a fixed admissible set $A$, and specializes to primitive recursive arithmetic when I take $A = HF$. (Something that would generalize PRA, rather than being analogous to PRA.) $\endgroup$ – Jacob Lurie Jan 28 '15 at 18:46
2
$\begingroup$

(This is more of a comment than an answer, but it's a bit too long to be split into comments so I'll post it as an answer.)

I don't know about functions defined on an arbitrary admissible set, but at least for admissible levels of the constructible hierarchy, you might be interested in what are called "$(\infty,0)$-recursive functions" in chapter VIII ("Recursion on Ordinals") of Peter G. Hinman's book Recursion-Theoretic Hierarchies (1978, available here), and also on this related question I asked a while ago while trying to make sense (without much success) of the various definitions. Hinman writes (op.cit., p.378) that:

The $(\infty,0)$-recursive functions will play somewhat the role here of the primitive recursive functions of ordinary recursion theory.

Perhaps even more relevant to your question would be the $(\infty,\lambda)$-recursive functions in Hinman's terminology, or even more the primitive $(\infty,\lambda)$-recursive functions in the terminology of the question I linked to, where $\lambda$ is the height of the admissible set considered (at least for a $L_\lambda$). But as I noted, the precise relation between these concepts escapes me.

Also somewhat relevant to your question might be Stephen G. Simpson's paper titled "Short Course on Admissible Recursion Theory" on p. 355–390 of Fenstad, Gandy & Sacks (eds.), Generalized Recursion Theory II (1978), proceedings of a symposium held in Oslo in 1977. It contains the clearest (if terse) explanation I found so far of how primitive recursive ordinal functions are defined and how they relate to more general recursion on ordinals.

$\endgroup$
0
$\begingroup$

Actually, for the case $\mathbb A$=$\mathbb H$$Y$$P_{\mathfrak M}$ (which seems, if I am understanding your question correctly, what you are referring to), since $\mathbb H$$F_{\mathfrak M}$$\subseteq$$\mathbb H$$Y$$P_{\mathfrak M}$, the generalization of primitive recursive function you get (rather than want, possibly) are the primitive computable functions of Moschovakis which are defined in his papers "Abstract First-Order Computability, I" and "Abstract First-Order computability, II". In fact, Thm. 2.6 in Chapter II of Barwise's book states that the $\Sigma_1$ relations on $\mathbb H$$F_{\mathfrak M}$ are semi-search computable on $\mathfrak M$ and the $\Delta_1$ relations on $\mathbb H$$F_{\mathfrak M}$ are the search-computable relations on $\mathfrak M$ (the search-computable relations being Moschovakis' generalization of the general recursive functions on $\mathfrak N$=(N,+,$\cdot$)) so what you seem to require, that is, that there exists a special class of "provably total" $\Sigma_1$ functions on $\mathbb A$ which reduces to the class of primitive recursive functions when $\mathbb A$=$\mathbb H$$F_{\mathfrak M}$ does not exist. That is why I asked those particular questions in my comment to you. If you believe my observation is incorrect, please be so kind as to show me how the class of functions you are interested in can exist.

$\endgroup$
  • 1
    $\begingroup$ I'm a little confused - what do you mean by " . . . the generalization of primitive recursive function you get . . ."? Get according to what process? Also, how do you get from Barwise' result to the statement that no such class exists? (I'm probably just missing something, but this isn't clear to me.) $\endgroup$ – Noah Schweber Feb 19 '15 at 23:13
  • 2
    $\begingroup$ I'm afraid that I don't follow either. What exactly are you saying you can rule out? $\endgroup$ – Jacob Lurie Feb 20 '15 at 1:55
  • $\begingroup$ @NoahS: If this helps any, the primitive, prime, and search computable functions of Moschovakis are defined over arbitrary first-order structures $\mathfrak M$ and are the analogues of the primitive recursive functions and general recursive functions over $\mathfrak N$=(N,+,$\cdot$). Prof. Lurie, in the second paragraph of his question, was interested in the admissible set $\mathbb A$=$\mathbb H$$Y$$P_{\mathfrak M}$ By the theorem I mentioned, the 'primitive recursive' functions over $\mathbb H$$F_{\mathfrak M}$ are the primitive computable functions of Moschovakis, $\endgroup$ – Thomas Benjamin Feb 20 '15 at 14:03
  • $\begingroup$ (cont.) not the primitive recursive functions over $\mathfrak N$=(N,+,$\cdot$). $\endgroup$ – Thomas Benjamin Feb 20 '15 at 14:06
  • $\begingroup$ This doesn't really address the question. It seems quite easy to define some theory $T_\mathbb{A}$ satisfied by $\mathbb{A}$ and some class of functions $F_\mathbb{A}$ on $\mathbb{A}$ such that (1) $T_\mathbb{A}$ prove sthat each $f\in F_\mathbb{A}$ is total and (2) $F_{HF}=PrimRec$. The question is whether there is a reasonably natural choice of such $T$ and $F$. When you bring up Moschovakis it seems you are homing on on specifically one approach, and then arguing that, if we follow that approach, no such class of functions exists (although even here I don't follow your reasoning); $\endgroup$ – Noah Schweber Feb 21 '15 at 1:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.