Good, I'll accept this answer which together with Qiaochu's comment goes a long way, even though there's perhaps room to say more about suspension H-spaces in the space of homotopy types rationally equivalent to odd spheres and in other homotopy theories (perhaps equivariantly). (BTW I of course meant $K(\mathbb Q,3)$ in the comment above.)

This is great! Just to expand a bit on the Adams-Walker construction, $Y$ is the homotopy colimit of a sequence of $S^3$s connected by the degree $i$ maps for all $i$ (is $Y=S^3_{\mathbb Q}$?), and it is thus the suspension of the corresponding sequence of $S^2$s. We only need that $S^3$ is an H-space to show that $Y$ is a $K(\mathbb Z,3)$, so a similar thing happens for a sequence of $S^7$s.

Thanks! I had a feeling there were very few choices, and this seems to confirm it. It is also in keeping with my feeling that there are probably no other non-trivial applications of this Cayley-Dickson-like construction (though I'd love to be proved wrong!).

To perhaps save someone else the trouble of searching the chapters, this is Cor. 6.14 in Ch. IV, p. 217.

Yes, I would also conjecture that (though I don't see at the moment how to prove it). And no, in Tait's “Intensional Interpretations of Functionals of Finite Type I”, several variants of T are defined either with propositional or predicate logic (and with extensions to accommodate bar recursion), with $\mathrm{T}_0'$ being close to Gödel's. He then considers directing the equations in order to study normalization, but this is not defining of the systems.

@ThomasBenjamin, OK, I've had a busy couple of days, but I'll put something up tomorrow.

System T interprets PA; it doesn't prove Con(PA). They are in this sense of equivalent strength: the recursive functions N→N represented by terms of System T are precisely the provably recursive functions of PA. A simple way to restrict System T so that you get just the primitive recursive functions is to allow only recursions with target type N (that is, you can still explicitly define and compose higher type functionals, but you cannot define those by recursion). Is that what you're after?

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.

I'm also aware that there are various approaches to finitism; e.g., under Kreisel's analysis it comes out to be equivalent with PA! But the system FA of Feferman-Strahm is fairly conservative: the logic is restricted to positive existential quantification over N. Maybe you would prefer a quantifier free presentation. In any case, with your proposal you run into the well-known problem with analyses of (any kind of) finitism that you want to go beyond the finite levels (!). Using unfolding avoids that quandary.

First, yes I'm aware that the Feferman-Schütte analysis of predicative concerns predicativity given the natural numbers. The unfolding of NFA is one way to approach that, and Feferman proposed that it should also be able to capture other notions of predicative closure, for instance of basic finitism (and in my dissertation, I study the unfolding of ID$_1$ which can model the predicative closure of one positive arithmetical inductive definition).

I found Eléments de logique $\Pi^1_n$ after all. But I don't know how to pronounce ptyx/ptykes nor why Girard picked the name. :) BTW, don't bother tracing the second volume of Girard's book, Proof theory and logical complexity; it never appeared (I hear there are drafts out there, but I haven't seen any).