4
$\begingroup$

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

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ Note that there's a crucial terminology distinction here (which I botched in a comment thread on the OP's prior question): primitive recursive function vs. primitive recursive functional. $\endgroup$
    – Noah Schweber
    Commented Oct 23, 2019 at 19:48
  • 2
    $\begingroup$ Incidentally, this cstheory.stackexchange answer looks relevant with regards to formulating the question more precisely - specifically, the difference between proving consistency and normalization. (There system F is talked about rather than system T, but at a glance I think the same issue holds.) $\endgroup$
    – Noah Schweber
    Commented Oct 23, 2019 at 19:56
  • $\begingroup$ It is interesting to note that in Girard's book PROOFS AND TYPES, Chapter 14 ("Strong normalization for $F$") one finds the following comment on pg. 113: "...Existence is much more delicate; in fact, we shall see in Chapter 15 that the normalization theorem for $F$ implies the consistency of second order arithmetic $PA_2$. The classic result of logic, if anything deserves that name, is Godel's second incompleteness theorem, which says (assuming that it is not contradictory) that the consistency of $PA_2$ cannot be proved within $PA_2$. Consequently, since consistency can be $\endgroup$
    – Thomas Benjamin
    Commented Oct 28, 2019 at 21:33
  • $\begingroup$ (cont.) deduced from normalization within $PA_2$, the normalization theorem cannot be proved within $PA_2$. That gives us an essential piece of information for the proof: we must look for a strategy which goes outside $PA_2$." Since the corollary, "All terms of $F$ are strongly normalisable" seems to be proven in a finite number of steps, strong normalisability is proven by finite means yet by means not provable in$PA_2$. Would these means be 'ideal' in Hilbert's sense? $\endgroup$
    – Thomas Benjamin
    Commented Oct 28, 2019 at 21:46
  • $\begingroup$ Note that what Girard means by "second-order arithmetic" is not the same as second-order Peano arithmetic - Girard's second-order arithmetic is a first-order theory. (In fact I think it's just Z$_2$.) $\endgroup$
    – Noah Schweber
    Commented Oct 28, 2019 at 21:47

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .