18
$\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).

Improve this question
$\endgroup$
6
  • 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$
    – Rachid Atmai
    Commented Jan 21, 2015 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
    Commented Jan 21, 2015 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
    Commented Jan 21, 2015 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
    Commented Jan 28, 2015 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
    Commented Jan 28, 2015 at 18:46

2 Answers 2

Reset to default
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.

Improve this answer
$\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.

Improve this answer
$\endgroup$
11
  • 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
    Commented Feb 19, 2015 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
    Commented Feb 20, 2015 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
    Commented Feb 20, 2015 at 14:03
  • $\begingroup$ (cont.) not the primitive recursive functions over $\mathfrak N$=(N,+,$\cdot$). $\endgroup$
    – Thomas Benjamin
    Commented Feb 20, 2015 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
    Commented Feb 21, 2015 at 1:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .