Timeline for What is the proof theoretic strength of PCF?
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 15, 2021 at 17:36 | comment | added | Sam Sanders | Have you checked Longley-Normann (Higher-order computability theory)? There is a discussion about PCF and its models. | |
| Apr 15, 2021 at 14:48 | comment | added | Not_Here | Sorry I don't mean a biinterpration, I mean a conservativity result. | |
| Apr 15, 2021 at 14:27 | comment | added | Not_Here | @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$. | |
| Apr 15, 2021 at 14:25 | comment | added | Not_Here | @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$ | |
| Apr 15, 2021 at 14:14 | comment | added | Fedor Pakhomov | 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)$. | |
| Apr 15, 2021 at 13:54 | history | asked | Not_Here | CC BY-SA 4.0 |