While doing some research on reverse mathematics, I came across the following document under the address, www.andrew.cmu.edu>user>avigad>Talks>survey1:

Proof theory and Subsystems of Second-Order Arithmetic

in which I found the following theorem and alleged proof, attributed to Godel (under the subheading, "The Dialectica interpretation"):

Theorem (Godel): The provably total recursive functions of $PA$ are exactly the primitive recursive functionals of type $\mathbb N$ $\rightarrow$ $\mathbb N$.

Proof: Write down a functional (quantifier-free) theory $T$ [presumably Godel's system $T$--my comment] whose terms denote the primitive recursive functionals of finite type. From a proof of

$\forall$ $x$$\exists$$y$$\varphi$($x$,$y$)

in $PA$, one can extract a term $f$ and a proof of

$\varphi$($x$, $f$($x$))

in $T$.

With this in mind, I ask the following question:

In which of the Big Five or their variants is Godel's System $T$ definable or equivalent to?

(Subsidiary questions: Is the statement of the theorem correct? Is it correctly attributable to Godel? Is the proof as stated correct?)

While doing some research on reverse mathematics, I came across the following document under the address, http://www.andrew.cmu.edu/user/avigad/Talks/survey1.pdf:

Proof theory and Subsystems of Second-Order Arithmetic

in which I found the following theorem and alleged proof, attributed to Godel (under the subheading, "The Dialectica interpretation"):

Theorem (Godel): The provably total recursive functions of $PA$ are exactly the primitive recursive functionals of type $\mathbb N$ $\rightarrow$ $\mathbb N$.

Proof: Write down a functional (quantifier-free) theory $T$ [presumably Godel's system $T$--my comment] whose terms denote the primitive recursive functionals of finite type. From a proof of

$\forall$ $x$$\exists$$y$$\varphi$($x$,$y$)

in $PA$, one can extract a term $f$ and a proof of

$\varphi$($x$, $f$($x$))

in $T$.

With this in mind, I ask the following question:

In which of the Big Five or their variants is Godel's System $T$ definable or equivalent to?

(Subsidiary questions: Is the statement of the theorem correct? Is it correctly attributable to Godel? Is the proof as stated correct?)

While doing some research on reverse mathematics, I came across the following document under the address, www.andrew.cmu.edu>user>avigad>Talks>survey1:

Proof theory and Subsystems of Second-Order Arithmetic

in which I found the following theorem and alleged proof, attributed to Godel (under the subheading, "The Dialectica interpretation"):

Theorem (Godel): The provably total recursive functions of $PA$ are exactly the primitive recursive functionals of type $\mathbb N$ $\rightarrow$ $\mathbb N$.

Proof: Write down a functional (quantifier-free) theory $T$ [presumably Godel's system $T$--my comment] whose terms denote the primitive recursive functionals of finite type. From a proof of

$\forall$ $x$$\exists$$y$$\varphi$($x$,$y$)

in $PA$, one can extract a term $f$ and a proof of

$\varphi$($x$, $f$($x$))

in $T$.

With this in mind, I ask the following question:

In which of the Big Five or their variants is Godel's System $T$ definable or equivalent to?

(Subsidiary questions: Is the statement of the theorem correct? Is it correctly attributable to Godel? Is the the proof as stated correct?)

While doing some research on reverse mathematics, I came across the following document under the address, www.andrew.cmu.edu>user>avigad>Talks>survey1:

Proof theory and Subsystems of Second-Order Arithmetic

in which I found the following theorem and alleged proof, attributed to Godel (under the subheading, "The Dialectica interpretation"):

Theorem (Godel): The provably total recursive functions of $PA$ are exactly the primitive recursive functionals of type $\mathbb N$ $\rightarrow$ $\mathbb N$.

Proof: Write down a functional (quantifier-free) theory $T$ [presumably Godel's system $T$--my comment] whose terms denote the primitive recursive functionals of finite type. From a proof of

$\forall$ $x$$\exists$$y$$\varphi$($x$,$y$)

in $PA$, one can extract a term $f$ and a proof of

$\varphi$($x$, $f$($x$))

in $T$.

With this in mind, I ask the following question:

In which of the Big Five or their variants is Godel's System $T$ definable or equivalent to?

(Subsidiary questions: Is the statement of the theorem correct? Is it correctly attributable to Godel? Is the proof as stated correct?)