Timeline for Numerical choice and reverse mathematics
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 10 at 9:56 | vote | accept | Sam Sanders | ||
| Oct 10 at 3:36 | answer | added | Dmytro Taranovsky | timeline score: 4 | |
| Oct 9 at 17:38 | history | became hot network question | |||
| Oct 9 at 17:36 | comment | added | Hanul Jeon | But also note that, this uniformization theorem does not guarantee the existence of a choice function (as you can see, a naive way to construct a choice function from $\hat{\phi}$ requires $\Pi^1_1$-comprehension.) | |
| Oct 9 at 17:34 | comment | added | Hanul Jeon | The point is that it is a uniformization not for real numbers, but for natural numbers. You may find its proof in Simpson's $\Sigma^1_1$ and $\Pi^1_1$ transfinite induction (Logic Colloquium '80, Stud. Logic Found. Math., 108), Lemma 2.3. | |
| Oct 9 at 17:30 | comment | added | Sam Sanders | @HanulJeon I thought that kind of uniformisation is only provable in $\Pi_1^1$-comprehension? | |
| Oct 9 at 17:28 | comment | added | Hanul Jeon | Relatedly, the numerical $\Pi^1_1$-uniformization theorem is a theorem of $\mathsf{ATR}_0$ (which states that if $\phi(x)$ is a $\Pi^1_1$-formula then we can find another $\Pi^1_1$-formula $\hat{\phi}(x)$ such that $\mathsf{ATR}_0$ proves $\forall^0 x [\hat{\phi}(x)\to\phi(x)]$ and $(\exists^0 x\phi(x))\to (\exists!^0 x \hat{\phi}(x))$. | |
| Oct 9 at 14:57 | answer | added | aws | timeline score: 4 | |
| Oct 9 at 14:12 | comment | added | Dmytro Taranovsky | The principle is provable in $Π^1_1-\text{CA}_0$, and its restriction to $m∈\{0,1\}$ is equivalent to $Σ^1_1$ separation and thus ATR$_0$. The upper bound version proves at least ACA$_0$. | |
| Oct 9 at 11:33 | comment | added | Sam Sanders | @aws Results in intuitionist logic would be fine too. | |
| Oct 9 at 11:22 | comment | added | aws | I assume you're thinking of classical logic? In intuitionistic logic there are some conservativity results in this area. | |
| Oct 9 at 9:37 | history | asked | Sam Sanders | CC BY-SA 4.0 |