It is well known that one can use Goedel's primitive recursive functionals of finite type to prove the consistency of $PA$ (Peano Arithmetic). As such, one can certainly use them to prove the consistency, say, of Primitive Recursive Arithmetic ($PRA$), but does one need the full 'power' (so to speak) of Goedels primitive recursive functionals to do so? In other words, what is a necessary and sufficient restriction of Goedel's primitive rcursive functionals that will prove just the consistency of $PRA$, and nothing else? My motivation for asking this question is to discover how 'small' the extension of the finitary standpoint has to be in order to prove the consistency of this weaker system. (Apologies in advance for the vagueness of the question.)

5$\begingroup$ I don't really understand what you're asking. What does it mean that a class of functionals proves that a theory is consistent? $\endgroup$– Noah SchweberJan 14, 2016 at 9:41

3$\begingroup$ Thanks, but that doesn't help me very much  can you define precisely what you mean? It sounds like you're asking how weak a theory with a certain form which proves that PRA is consistent can be; is this right? If so, what's that form? $\endgroup$– Noah SchweberJan 14, 2016 at 13:08

2$\begingroup$ 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? $\endgroup$– Ulrik BuchholtzJan 14, 2016 at 18:01

2$\begingroup$ What the OP probably means to say is that strong normalization of System $T$ implies consistency of $PA$. And so the question is how to restrict System $T$ so that strong normalization of the restricted system implies consistency of $PRA$ but is too weak to imply consistency of $PA$. $\endgroup$– Andrej BauerJan 21, 2016 at 11:01

1$\begingroup$ To go from probably to certainly I would like to see a proof. As to your other question, it ought to be similar to the reasoning done by Gödel in Dialectica: if there were a term corresponding to a proof of $\bot$ then there would also exist a normal term corresponding to $\bot$, but there isn't one. $\endgroup$– Andrej BauerJan 21, 2016 at 15:45
1 Answer
Sorry for taking a bit longer to answer: Everything I say here is from Jeremy Avigad and Sol Feferman's article in the Handbook of Proof Theory, Gödel’s functional (“Dialectica”) interpretation: http://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf
First let me note that PRA itself is an answer to the question as stated, namely a subsystem of System T whose consistency implies that of PRA :P
However, a number of issues came up in the comments, so I'll try to say something more. First, I'll discuss the situation for System T and PA, then some corresponding results for PRA.
By Theorem 3.2.1, a weak base theory proves Con(T) → Con(PA). This is the result for which we seek an analogue for PRA. The weak base theory here means a subsystem of PRA, almost certainly EFA (elementary function arithmetic) would suffice.
In the comments, the issue was raised regarding the connection between normalization of the terms of T and consistency of T. We have that Norm(T) → Con(T), because confluence can be proved in a weak base theory. This is discussed after Lemma 4.3.1. I don't believe we can hope for the reverse implication, Con(T) → Norm(T), though.
The facts about terms and provably total recursive functions (ptrf's) are in Corollary 3.2.4 (every ptrf of PA is denoted by a term of T) and Theorem 4.3.3 (for every term $t$ of T, PA proves that $t$ is normalizing; if $t$ has type $\mathbb N\to\mathbb N$, we can then get a ptrf $e$ by formalizing the reduction behavior of $t$).
Now let's move to systems of strength PRA:
A system that is very similar to what I described in my comment, $\hat{\mathrm{T}}$, is defined Section 5.1 (with a reference to Kleene 1959). Theorem 5.1.1 describes a translation of terms of $\hat{\mathrm{T}}$ into terms of PRA such that if $\hat{\mathrm{T}}$ derives an equation, then PRA derives the translated equation. This can presumably be formalized in EFA, so that EFA proves Con(PRA) → Con($\hat{\mathrm{T}}$). Note that PRA is actually a subtheory of $\hat{\mathrm{T}}$, so Con($\hat{\mathrm{T}}$) → Con(PRA) is automatic (cf. the remark in the beginning of this answer).
Avigad and Feferman do not discuss normalization for $\hat{\mathrm{T}}$, but I would conjecture that for every term $t$ of $\hat{\mathrm{T}}$, PRA proves that $t$ is normalizing.
(Note that the highlight of Section 5 is actually some results for $\mathrm{I\Sigma}_1$, notably conservativity over PRA and that every ptrf is primitive recursive (denoted by a term of PRA, if you will).)

$\begingroup$ Do you think that for every term $t$ of $T$hat strong normalization is provable in $PRA$? $\endgroup$ Jan 29, 2016 at 13:12

$\begingroup$ Also, in Tait's 1967 paper, I understand that he defined System $T$ as a set of rewrite rules. Is this correct? $\endgroup$ Jan 29, 2016 at 13:16

$\begingroup$ 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. $\endgroup$ Jan 29, 2016 at 14:39