Timeline for Impredicativity, definition, recursion and conservatism
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 17, 2023 at 0:42 | comment | added | Andreas Blass | @FrodeAlfsonBjørdal Yes, that definition of $G$ looks good (assuming of course that $A$ describes a monotone operation). | |
| Oct 16, 2023 at 23:59 | comment | added | Frode Alfson Bjørdal | Do we agree, then, that $\forall x(Gx\leftrightarrow\forall K((A(K,x)\to Kx)\to Kx))$ is a recursive definition of G? | |
| Sep 21, 2023 at 0:07 | comment | added | Andreas Blass | If you add to $ACA_0$ an axiom saying that every arithmetical operator $A$ has a least fixed point, then you can obtain a $\Pi^1_1$-complete set as a fixed point, so the system would be at least as strong as $\Pi^1_1$-$CA_0$. If you only added existence of a fixed point but not minimality, then I'd expect the result to be $ATR_0$ or nearby. So in either case, I don't expect conservativity over $ACA_0$. | |
| Sep 21, 2023 at 0:00 | comment | added | Frode Alfson Bjørdal | Suppose T is ACA_0 + $\forall x(Gx\leftrightarrow A(x,G))$. May not T be stronger than ACA_0, so that $\forall x(Gx\leftrightarrow A(x,G))$ is not conservative? | |
| Sep 20, 2023 at 23:58 | vote | accept | Frode Alfson Bjørdal | ||
| Sep 20, 2023 at 22:59 | history | answered | Andreas Blass | CC BY-SA 4.0 |