What restriction(s) of Goedel's primitive recursive functionals is (are) necessary and sufficient to prove the consistency of $PRA$

Question

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.)

Answer 1

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).)