1
$\begingroup$

Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic higher-order functionals of finite type closed under higher-order primitive recursion, which can be given as the natural extension of $PRA$ to higher-order functionals of finite type. To a type theorist or someone working in programming language foundations, $T$ is an extension of the simply typed lambda calculus, given by adding typing rules for the natural numbers, higher order functionals, and zero, successor, and primitive recursion on the functionals. Again, it is clear how these are distinct and yet equivalent formulations. As is well known, the proof theoretic strength of $T$ is equivalent to that of $PA$.

Dana Scott introduced a system now called $PCF$ (c.f. this note on Wikipedia for the relevant history), which is an extension of the simply typed lambda calculus in the same way as $T$, and is defined the same ways as $T$ is but with the addition of some mechanism, usually the fixedpoint Y combinator, to allow for general recursion of the higher-order functionals. Thus the difference between $T$ and $PCF$ is the difference between primitive and general recursion, and as a result $PCF$ breaks $T$'s strong normalization/termination property.

What is the proof theoretic strength of $PCF$, that is, $T$ + a mechanism for higher-order general recursion? I have been looking through the literature to see if this is known and the only thing I could find was section 8 of Avigad and Feferman's paper on $T$, where they introduce a $\mu$ operator that converts all arithmetical formulae to a quantifier free form and derive the proof theoretic strength of $T + \mu$, but I cannot follow the arguments of some of that section and if a higher-order general recursion scheme is derivable from $\mu$ (which would make sense given the name), then I am having trouble seeing that argument. Is the argument a higher-order analog of Kleene's normal form theorem?

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ I am not really familiar with $PCF$ (only checked your Wikipedia link). But are you sure that it even makes sense to ask about the proof theoretic ordinal of $PCF$? For example, as far as I understand, for untyped lambda calculus it wouldn't make sense to ask about its proof-theoretic ordinal. In the case of $T+\mu$ we could ask about the consistency strength, i.e. the amount of transfinite induction one needs to show that $T+\mu\nvdash 0=S(0)$. $\endgroup$
    – Fedor Pakhomov
    Commented Apr 15, 2021 at 14:14
  • $\begingroup$ @FedorPakhomov I tried to outline the different ways of formulating the system by using the two different ways of looking at $T$ above, but perhaps I wasn't clear. It does make sense to ask about the proof theoretic strength of $PCF$ in the same way it makes sense to ask about $T$, and that result is achieved via Godel's Dialectica interpretation of PA in $T$. I'm asking about the strength of $PCF$ as a first order quantifier free equational theory of arithmetical higher order functionals and a general recursion operator, which can be given by its biinterpretation with a fragment of $Z_2$ $\endgroup$
    – Not_Here
    Commented Apr 15, 2021 at 14:25
  • $\begingroup$ @FedorPakhomov Consistency strength is also a perfectly coherent question, but the comparison to untyped lambda calculus doesn't make sense because $PCF$ is a typed extension of the simply typed lambda calculus, just like $T$. $\endgroup$
    – Not_Here
    Commented Apr 15, 2021 at 14:27
  • $\begingroup$ Sorry I don't mean a biinterpration, I mean a conservativity result. $\endgroup$
    – Not_Here
    Commented Apr 15, 2021 at 14:48
  • 1
    $\begingroup$ Have you checked Longley-Normann (Higher-order computability theory)? There is a discussion about PCF and its models. $\endgroup$
    – Sam Sanders
    Commented Apr 15, 2021 at 17:36

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .