Timeline for The difference between Baire 2 and 'effectively Baire 2'
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 20, 2022 at 18:31 | comment | added | Sam Sanders | I am not saying that $\exists^3$, which does imply $Z_2$, is required: the former is just the weakest comprehension functional that computes (S1-S9) the operation on input a function $f$ of bounded variation, output a sequence of continuous functions that pointwise converges to $f$. And an honest question: why do we not compute (S1-S9) with third-order functions, while we do (Turing) compute with "definable classes coding a pointwise convergent sequence of graphs of Baire-1 functions"? Even if S1-S9 seems complicated, the coding is too, and similar coding has to be done each time. | |
| Dec 20, 2022 at 17:04 | comment | added | Elliot Glazer | Certainly one would need full $Z_2$ to prove the scheme assigning every definable class coding a pointwise convergent sequence of graphs of Baire-1 functions to a formula defining a double sequence of polynomials which effectively represents the limit Baire-2 function. | |
| Dec 20, 2022 at 16:43 | comment | added | Elliot Glazer | What I'm proposing might be doable in $\Pi^1_1-CA_0$ is showing that the formula defined in this construction sends each pointwise convergence sequence of continuous functions to the canonical sequence of rational polynomials with same pointwise limit. This is a single sentence, so it can only use a finite fragment of $Z_2.$ What would require full $Z_2$ is the theorem scheme which provides every formula which defines the graph of a Baire-1 function a formula defining its canonical rational polynomial sequence. | |
| Dec 20, 2022 at 14:20 | comment | added | Sam Sanders | In Kleene's S1-S9 computability theory, the operation on input a function $f$ of bounded variation, output a sequence of continuous functions that pointwise converges to $f$ cannot be done with comprehension functionals less than Kleene's $\exists^3$, which implies full $Z_2$. This shows a big difference between computing with second-order codes and third-order objects. Hence, one should be careful with claims about $\Pi_1^1$-comprehension etc. See here for details: academic.oup.com/logcom/article-abstract/32/8/1747/6833330 | |
| Dec 20, 2022 at 11:08 | comment | added | Elliot Glazer | @SamSanders In the language of $Z_2,$ you can consider the equivalence relation of $r_1 \sim r_2$ if both reals code sequences of continuous functions which converge to the same output at each $x.$ Then the construction given provides canonical representatives of each equivalence class. | |
| Dec 20, 2022 at 11:04 | comment | added | Sam Sanders | Thanks for the nice answer! You mention that your construction can be carried out in $Z_2$. How do you assume the Baire 1 function is given in the language of second-order arithmetic? | |
| Dec 20, 2022 at 10:59 | vote | accept | Sam Sanders | ||
| Dec 20, 2022 at 10:08 | history | answered | Elliot Glazer | CC BY-SA 4.0 |