Timeline for What notable theorems cannot be automatically proven without choice using Shoenfield absoluteness?
Current License: CC BY-SA 4.0
17 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 12, 2023 at 20:05 | comment | added | Asaf Karagila♦ | arxiv.org/abs/2204.00247 and arxiv.org/abs/1402.3048 seem related. | |
| Sep 11, 2023 at 8:11 | answer | added | Elliot Glazer | timeline score: 22 | |
| Sep 10, 2023 at 2:47 | comment | added | Timothy Chow | @JamesHanson Unfortunately, I don't know of any examples. | |
| Sep 10, 2023 at 1:23 | history | became hot network question | |||
| Sep 9, 2023 at 20:37 | comment | added | James E Hanson | @TimothyChow Incidentally, do you know of any example regarding question 1 that have been studied in the context of reverse math? | |
| Sep 9, 2023 at 20:33 | comment | added | James E Hanson | @TimothyChow I do agree that learning how to spot projective quantifier complexity and learning how to code thing in second-order arithmetic are roughly equivalent, so you're right that it would be of comaprable difficulty. I just think that the convenience of having access to big objects is real and mathematicians have demonstrated that there is conceptual utility in using less tangible objects to prove things about more tangible objects. | |
| Sep 9, 2023 at 19:41 | comment | added | Timothy Chow | @JamesHanson I see. It doesn't strike me as easier to train oneself to determine quantifier complexity than to learn something about reverse mathematics and subsystems of second-order arithmetic, and the latter has the advantage that you can tap into an entire community of people who are dedicated to answering questions of this type. But I suppose it could seem easier to some people. | |
| Sep 9, 2023 at 18:38 | comment | added | James E Hanson | ...are low enough on the projective hierarchy for absoluteness to be applicable, b) proofs using big objects are often conceptually simpler than careful proofs that stay inside the reals or at the very least having the option of resorting to a big object is useful (otherwise normal mathematicians wouldn't use things like dual spaces and Grothendieck universes), and c) working without choice or even just being careful about what choice you use can be a pain (which is why mainstream mathematicians largely gave up on trying to do it). | |
| Sep 9, 2023 at 18:38 | comment | added | James E Hanson | @TimothyChow Not exactly. I feel like my point is really this: The only 'constructive' theory on a lot of mathematicians' and physicists' radar is ZF. Assuming that you would be happier if results were provable in ZF alone and you aren't a set theorist, then I'd argue that the easiest course of action is to get a feel for the quantifier complexity of projective statements (which I don't think is really that hard) and liberally use absoluteness when you can. I think this is the best course because a) I think most mathematical statements that 'feel' tangible... | |
| Sep 9, 2023 at 18:22 | comment | added | Timothy Chow | @JamesHanson Can we rephrase your philosophical point as follows? Some who is worried about AC and who really only cares about "tangible" statements would be well-advised to use second-order arithmetic (rather than set theory) as a foundation. Doing so would eliminate all concerns about AC from the get-go; there would be no need to spend half of one's life tediously checking whether this or that result uses AC. | |
| Sep 9, 2023 at 17:52 | answer | added | Noah Schweber | timeline score: 11 | |
| Sep 9, 2023 at 17:49 | comment | added | Joel David Hamkins | So one is using slightly less than ZFC provability of the $\Pi^1_4$ assertion $\forall x\varphi(x)$, since it suffices that $\varphi(a)$ holds in every $L[a]$. | |
| Sep 9, 2023 at 17:39 | comment | added | Noah Schweber | Ah, yes. Silly moment. Meanwhile, if $\mathsf{ZFC}$ proves a $\Sigma^1_4$ sentence $\exists r\varphi$ (with $\varphi$ being $\Pi^1_3$), we do get in each $L[a]$ a real $b$ which $L[a]$ thinks satisfies $\varphi$, but we can't a priori lift any of those up to $V$ since $\varphi$ is too complicated. I think I was getting my directions of absoluteness confused. | |
| Sep 9, 2023 at 17:32 | comment | added | James E Hanson | @NoahSchweber Let $\varphi(x)$ be a $\Sigma^1_3$ formula with no parameters. Suppose $\mathsf{ZFC}$ proves $\forall x \varphi(x)$. Then for any real $a$, $L[a] \models \varphi(a)$. Since $\Sigma^1_3$ formulas are upwards absolute, we have that $V \models \varphi(a)$. Since we can do this for any $a$, we have that $V \models \forall x \varphi(x)$. | |
| Sep 9, 2023 at 17:29 | comment | added | Noah Schweber | I'm actually slightly confused; how do you get full $\Pi^1_4$ absoluteness between $\mathsf{ZFC}$ and $\mathsf{ZF}$? The best I can see is $\Pi^1_3$ (or does "explicitly given $\Pi^1_4$" mean something subtle?). | |
| Sep 9, 2023 at 17:27 | comment | added | Noah Schweber | Somewhat related: math.stackexchange.com/questions/3491349/… | |
| Sep 9, 2023 at 17:20 | history | asked | James E Hanson | CC BY-SA 4.0 |